Use new typecheck stuff, to be added to all trees

src/main/scala/leon/purescala/Trees.scala

@@ -79,11 +79,7 @@ object Trees {
   case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr with FixedType with ScalacPositional {
     val fixedType = funDef.returnType
 
-    funDef.args.zip(args).foreach{ case (a, c) =>
-      if (!isSubtypeOf(c.getType, a.tpe)) {
-        throw new TypeErrorException("Invalid invocation of "+funDef.id+": argument "+a.id+":"+a.tpe+" was passed "+c+":"+c.getType)
-      }
-    }
+    funDef.args.zip(args).foreach{ case (a, c) => typeCheck(c, a.tpe) }
   }
   case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr