diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index b89735441018a565c78ff49fa13eaa104f0d845c..4f51d8c05866273cc15b659b5a54b562dee797d4 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -73,7 +73,7 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80)
 
             val newFun = new FunDef(FreshIdentifier("rec", true), tpe, Seq(VarDecl(inductOn, inductOn.getType)))
             newFun.precondition = Some(preIn)
-            newFun.postcondition = Some(And(Equals(ResultVariable(), Tuple(p.xs.map(Variable(_)))), p.phi))
+            newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable(), p.phi))
 
             newFun.body = Some(
               IfExpr(Equals(Variable(inductOn), IntLiteral(0)),
@@ -248,7 +248,7 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
             val outerPre = Or(globalPre)
 
             newFun.precondition = Some(funPre)
-            newFun.postcondition = Some(And(Equals(ResultVariable(), Tuple(p.xs.map(Variable(_)))), p.phi))
+            newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable(), p.phi))
 
             newFun.body = Some(MatchExpr(Variable(inductOn), cases))