diff --git a/src/cp/Converter.scala b/src/cp/Converter.scala
index 98772f4086433bbfcb4a961422749544da7907fb..559308e34a43edcb1eafee197d53d8141f970f56 100644
--- a/src/cp/Converter.scala
+++ b/src/cp/Converter.scala
@@ -10,4 +10,7 @@ class Converter(expr2scala : (Expr => Any)) {
 
   def exprSeq2scala2[A,B](exprs: Seq[Expr]) : (A,B) =
     (expr2scala(exprs(0)).asInstanceOf[A], expr2scala(exprs(1)).asInstanceOf[B])
+
+  def exprSeq2scala3[A,B,C](exprs: Seq[Expr]) : (A,B,C) =
+    (expr2scala(exprs(0)).asInstanceOf[A], expr2scala(exprs(1)).asInstanceOf[B], expr2scala(exprs(2)).asInstanceOf[C])
 }
diff --git a/src/cp/Terms.scala b/src/cp/Terms.scala
index 7b4bc16e88c0313582bf19dea7c7174a48d08675..4ba948c20d7ad0a735b87db5e9cf1445e537d495 100644
--- a/src/cp/Terms.scala
+++ b/src/cp/Terms.scala
@@ -220,22 +220,19 @@ object Terms {
   /********** TERM METHODS **********/
   /** compose_i_j_k will compose f (of arity j) and g (of arity k) as "g∘f" by
    * inserting arguments of f in place of argument i of g */
-  private def compose_0_1_1[T1,T2,T3](f : Term[T1,T2], g : Term[T2,T3]) : Term1[T1,T3] = {
+  private def compose_0_1_1[A1,R1,R2](f : Term[(A1),R1], g : Term[(R1),R2]) : Term1[A1,R2] = {
     val (newExpr, newTypes) = compose(f, g, 0, 1, 1)
     Term1(f.program, newExpr, newTypes, f.converter)
   }
-
-  private def compose_0_2_1[T1,T2,R1,R2](f : Term[(T1,T2),R1], g : Term[R1,R2]) : Term2[T1,T2,R2] = {
+  private def compose_0_2_1[A1,A2,R1,R2](f : Term[(A1,A2),R1], g : Term[(R1),R2]) : Term2[A1,A2,R2] = {
     val (newExpr, newTypes) = compose(f, g, 0, 2, 1)
     Term2(f.program, newExpr, newTypes, f.converter)
   }
-
-  private def compose_0_1_2[T1,R1,T2,R2](f : Term[T1,R1], g : Term[(R1,T2),R2]) : Term2[T1,T2,R2] = {
+  private def compose_0_1_2[A1,R1,B2,R2](f : Term[(A1),R1], g : Term[(R1,B2),R2]) : Term2[A1,B2,R2] = {
     val (newExpr, newTypes) = compose(f, g, 0, 1, 2)
     Term2(f.program, newExpr, newTypes, f.converter)
   }
-
-  private def compose_1_1_2[T1,R1,T2,R2](f : Term[T1,R1], g : Term[(T2,R1),R2]) : Term2[T2,T1,R2] = {
+  private def compose_1_1_2[A1,R1,B1,R2](f : Term[(A1),R1], g : Term[(B1,R1),R2]) : Term2[B1,A1,R2] = {
     val (newExpr, newTypes) = compose(f, g, 1, 1, 2)
     Term2(f.program, newExpr, newTypes, f.converter)
   }
@@ -255,7 +252,7 @@ object Terms {
 
       val indexToReplace = deBruijnG(index)
       val newExpr   = replace(Map(indexToReplace -> renamedExprF), renamedExprG)
-      val newTypes  = g.types.take(index) ++ f.types ++ g.types.drop(index + nf)
+      val newTypes  = g.types.take(index) ++ f.types ++ g.types.drop(index + 1)
       assert(newTypes.size == nf + ng - 1)
       (newExpr, newTypes)
     }
diff --git a/src/cp/Utils.scala b/src/cp/Utils.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c960a373e50f2c0cf5001044cb5dc41ba4c301c8
--- /dev/null
+++ b/src/cp/Utils.scala
@@ -0,0 +1,48 @@
+package cp
+
+object Utils {
+
+  /** Generate `compose' methods for terms */
+  object GenerateCompose {
+    private def indent(s : String) : String = s.split("\n").mkString("  ", "\n  ", "")
+
+    def apply(maxArity : Int) : String = {
+      val methods : Seq[String] = (for (arityG <- 1 to maxArity) yield {
+        for (arityF <- 1 to (maxArity - arityG + 1)) yield {
+          for (index <- 0 until arityG) yield {
+            val sb = new scala.collection.mutable.StringBuilder
+            sb.append("private def compose_")
+            sb.append(index + "_" + arityF + "_" + arityG)
+            val fParams = (1 to arityF).map("A" + _)
+            val gParams = (1 to arityG).map("B" + _)
+
+            val replacedGParams = gParams.take(index) ++ Seq("R1") ++ gParams.drop(index + 1)
+            val allParams = fParams ++ Seq("R1") ++ (gParams.take(index) ++ gParams.drop(index + 1)) ++ Seq("R2")
+
+            sb.append(allParams.mkString("[", ",", "]"))
+
+            sb.append("(f : Term[")
+            sb.append(fParams.mkString("(", ",", ")"))
+            sb.append(",R1], g : Term[")
+            sb.append(replacedGParams.mkString("(", ",", ")"))
+            sb.append(",R2]) : Term")
+
+            val newTermSize = arityG + arityF - 1
+            val resultParams = gParams.take(index) ++ fParams ++ gParams.drop(index + 1) ++ Seq("R2")
+
+            sb.append(resultParams.mkString(newTermSize + "[", ",", "]"))
+            sb.append(" = {\n")
+            sb.append(indent("val (newExpr, newTypes) = compose(f, g, " + index + ", " + arityF + ", " + arityG + ")"))
+            sb.append("\n")
+            sb.append(indent("Term" + newTermSize + "(f.program, newExpr, newTypes, f.converter)"))
+            sb.append("\n")
+            sb.append("}")
+            sb.toString
+          }
+        }
+      }).flatten.flatten
+
+      methods.mkString("\n")
+    }
+  }
+}