diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 0e7493018c8aef6e52d0a894c8bafaa5ae89ab17..f64c0521985846e8a8ff17f2c83d64ac34e4b7f4 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -300,6 +300,14 @@ object TypeOps {
             val mapping = args.map(_.id) zip newArgs.map(_.id)
             Lambda(newArgs, rec(idsMap ++ mapping)(body)).copiedFrom(l)
 
+          case f @ Forall(args, body) =>
+            val newArgs = args.map { arg =>
+              val tpe = tpeSub(arg.getType)
+              ValDef(freshId(arg.id, tpe))
+            }
+            val mapping = args.map(_.id) zip newArgs.map(_.id)
+            Forall(newArgs, rec(idsMap ++ mapping)(body)).copiedFrom(f)
+
           case p @ Passes(in, out, cases) =>
             val (newIn, newCases) = onMatchLike(in, cases)
             passes(newIn, srec(out), newCases).copiedFrom(p)