diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 4eb938d2fca5d500b0e0326b3442173287c76ba6..24e54b367f982c37a8b0d539c0fa1c40e73f7f47 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -413,13 +413,32 @@ object ExprOps extends GenTreeOps[Expr] {
     def simplerLet(t: Expr): Option[Expr] = t match {
 
       /* Untangle */
+      case Let(i1, Let(i2, e2, b2), b1) =>
+        Some(Let(i2, e2, Let(i1, b2, b1)))
+
+      case Let(i1, LetTuple(is2, e2, b2), b1) =>
+        Some(letTuple(is2, e2, Let(i1, b2, b1)))
+
+      case LetTuple(ids1, Let(id2, e2, b2), b1) =>
+        Some(Let(id2, e2, letTuple(ids1, b2, b1)))
+
       case LetTuple(ids1, LetTuple(ids2, e2, b2), b1) =>
         Some(letTuple(ids2, e2, letTuple(ids1, b2, b1)))
 
-      case Let(i1, Let(i2, e2, b2), b1) =>
-        Some(Let(i2, e2, Let(i1, b2, b1)))
+      // Untuple
+      case Let(id, Tuple(es), b) =>
+        val tps = es map (_.getType)
+        val ids = tps.zipWithIndex.map {
+          case (tp, ind) => FreshIdentifier(id + (ind + 1).toString, tp, true)
+        }
+        val theMap: Map[Expr, Expr] = es.zip(ids).zipWithIndex.map {
+          case ((e, subId), ind) => TupleSelect(Variable(id), ind + 1) -> Variable(subId)
+        }.toMap
+
+        val replaced0 = replace(theMap, b)
+        val replaced  = replace(Map(Variable(id) -> Tuple(ids map Variable)), replaced0)
 
-      // TODO
+        Some(letTuple(ids, Tuple(es), replaced))
 
       case Let(i, e, b) if freeComputable(e) && isPurelyFunctional(e) =>
         // computation is very quick and code easy to read, always inline