diff --git a/CHANGES.md b/CHANGES.md
index 7c91b4b7..0c830101 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,4 +1,5 @@
 ## Catt
+- Computation of Eckmann-Hilton cells as a builtin
 - Improve efficiency by storing partially checked terms
 - Computation of cylinder compositions as a builtin
 - Computation of cone compositions as a builtin
diff --git a/examples/eckmann-hilton-versions/higher-eh/eh-3-0.catt b/examples/eckmann-hilton-versions/higher-eh/eh-3-0.catt
new file mode 100644
index 00000000..34490878
--- /dev/null
+++ b/examples/eckmann-hilton-versions/higher-eh/eh-3-0.catt
@@ -0,0 +1,245 @@
+let 1paddedL (x : *) (y : *)
+    	     (f : x -> x) (g : x -> y)
+	     = comp f g
+
+coh 2padL (x(f)y) : f -> 1paddedL (id x) f
+
+let 1paddedU (x : *)
+    	     (f : x -> x) (g : x -> x)
+    	     = comp f g
+
+coh 2padU (x) : id x -> 1paddedU (id x) (id x)
+
+coh bias (x) : 2padU x -> 2padL (id x)
+
+coh Ibias (x) : I (2padU x) -> I (2padL (id x))
+
+let 2paddedL (x : *) (y : *)
+    	     (f : x -> y) (g : x -> y)
+	     (a : id x -> id x) (b : f -> g)
+	     = comp (2padL f) (1paddedL [a] [b]) (I (2padL g))
+
+coh 3padL (x(f(a)g)y) : a -> 2paddedL (id (id x)) a
+
+let 2paddedU (x : *)
+    	     (a : id x -> id x) (b : id x -> id x)
+    	     = comp (2padU x) (1paddedU [a] [b]) (I (2padU x))
+
+coh 3padU (x) : id (id x) -> 2paddedU (id (id x)) (id (id x))
+
+let 3paddedL (x : *) (y : *)
+    	     (f : x -> y) (g : x -> y)
+	     (a : f -> g) (b : f -> g)
+	     (p : id (id x) -> id (id x)) (q : a -> b)
+	     = comp (3padL a) (2paddedL [p] [q]) (I (3padL b))
+	     
+coh 4padL (x(f(a(p)b)g)y) : p -> 3paddedL (id (id (id x))) p
+
+
+let 3paddedU (x : *)
+    	     (p : id (id x) -> id (id x)) (q : (id (id x)) -> (id (id x)))
+    	     = comp (3padU x) (2paddedU [p] [q]) (I (3padU x))
+
+coh 4padU (x) : id (id (id x)) -> 3paddedU (id (id (id x))) (id (id (id x)))
+
+let 4paddedL (x : *) (y : *)
+    	     (f : x -> y) (g : x -> y)
+	     (a : f -> g) (b : f -> g)
+	     (p : a -> b) (q : a -> b)
+	     (m : id (id (id x)) -> id (id (id x))) (n : p -> q)
+	     = comp (4padL p) (3paddedL [m] [n]) (I (4padL q))
+
+coh 5padL (x(f(a(p(m)q)b)g)y) : m -> 4paddedL (id (id (id (id x)))) m
+
+let 4paddedU (x : *)
+    	     (m : id (id (id x)) -> id (id (id x))) (n : id (id (id x)) -> id (id (id x)))
+	     = comp (4padU x) (3paddedU [m] [n]) (I (4padU x))
+
+coh 5padU (x) : id (id (id (id x))) -> 4paddedU (id (id (id (id x)))) (id (id (id (id x))))
+
+
+coh focus-33-to-middle2 (x0(f1)x1(f2)x2(f3)x3(f4)x4(f5)x5(f6)x6) :
+    comp (comp f1 f2 f3) (comp f4 f5 f6) -> comp f1 f2 (comp f3 f4) f5 f6
+
+coh factor3padL (x) : 3padL (id (id x)) -> comp (3padU x) (comp [bias x] (comp [id (id x)] [id (id x)]) [Ibias x])
+
+coh unfactor3padU (x) : comp (comp [bias x] (comp [id (id x)] [id (id x)]) [Ibias x])
+    		      	     (I (3padL (id (id x))))
+			     -> I (3padU x)
+
+coh burger (x(f(a)g)y(h)z(j(b)k)w) : comp f h j -> comp g h k
+
+let nat-of-id-WRT-bias (x : *) (y : *) (z : *) (w : *)
+    		       (f1 : x -> y) (f2 : x -> y) (g1 : y -> z) (g2 : y -> z) (h1 : z -> w) (h2 : z -> w)
+		       (a : f1 -> f2) (b : g1 -> g2) (c : h1 -> h2) 
+		       = burger a [b] c
+
+let middlestep1 (x : *) = comp [factor3padL x] (2paddedL [id (id (id x))] [id (id (id x))]) (I (3padL (id (id x))))
+
+coh focus-first2-to-middle2 (x0(f1)x1(f2)x2(f3)x3(f4)x4) : comp (comp f1 f2) f3 f4 -> comp f1 (comp f2 f3) f4
+
+let middlestep2 (x : *) 
+    		= focus-first2-to-middle2 (3padU x)
+		  			  (burger (bias x) (comp [id (id x)] [id (id x)]) (Ibias x))
+					  (2paddedL [id (id (id x))] [id (id (id x))])
+					  (I (3padL (id (id x))))
+
+let middlestep3 (x : *)
+    		= comp (3padU x) [nat-of-id-WRT-bias (bias x) (comp [[id (id (id x))]] [[id (id (id x))]]) (Ibias x)]  (I (3padL (id (id x))))
+
+coh focus-middle2-to-last2 (x0(f1)x1(f2)x2(f3)x3(f4)x4) : comp f1 (comp f2 f3) f4 -> comp f1 f2 (comp f3 f4)
+
+let middlestep4 (x : *)
+    		= focus-middle2-to-last2 (3padU x)
+		  			 (2paddedU [id (id (id x))] [id (id (id x))])
+		  		 	 (burger (bias x) (comp [id (id x)] [id (id x)]) (Ibias x))
+					 (I (3padL (id (id x))))
+
+let middlestep5 (x : *)
+    		= comp (3padU x) (2paddedU [id (id (id x))] [id (id (id x))]) [unfactor3padU x]
+
+let middle (x : *)
+    	   = comp (middlestep1 x)
+	     	  (middlestep2 x)
+		  (middlestep3 x)
+		  (middlestep4 x)
+		  (middlestep5 x)
+		  (I (op { 1 } (middlestep5 x)))
+		  (I (op { 1 } (middlestep4 x)))
+		  (I (op { 1 } (middlestep3 x)))
+		  (I (op { 1 } (middlestep2 x)))
+		  (I (op { 1 } (middlestep1 x)))
+
+coh middlereplace (x) : comp (I (4padL (id (id (id x))))) (op { 1 } (4padL (id (id (id x))))) -> middle x
+
+let step1 (x : *)
+    	  (m : id (id (id x)) -> id (id (id x)))
+	  (n : id (id (id x)) -> id (id (id x)))
+	  = comp [5padL m] [op { 1 } (5padL n)]
+
+let step2 (x : *)
+    	  (m : id (id (id x)) -> id (id (id x)))
+	  (n : id (id (id x)) -> id (id (id x)))
+	  = focus-33-to-middle2 (4padL (id (id (id x))))
+	    		    	(3paddedL [id (id (id (id x)))] [m])
+			    	(I (4padL (id (id (id x)))))
+			   	(op { 1 } (4padL (id (id (id x)))))
+			    	(op { 1 } (3paddedL [id (id (id (id x)))] [n]))
+			    	(op { 1 } (I (4padL (id (id (id x))))))
+let step3 (x : *)
+    	  (m : id (id (id x)) -> id (id (id x)))
+	  (n : id (id (id x)) -> id (id (id x)))
+	  = comp  (4padL (id (id (id x))))
+	    	  (3paddedL [id (id (id (id x)))] [m])
+		  [middlereplace x]
+		  (op { 1 } (3paddedL [id (id (id (id x)))] [n]))
+		  (op { 1 } (I (4padL (id (id (id x))))))
+		  
+coh focus-2-3-and-12-13 (x0(f1)x1(f2)x2(f3)x3(f4)x4(f5)x5(f6)x6(f7)x7(f8)x8(f9)x9(f10)x10(f11)x11(f12)x12(f13)x13(f14)x14)
+    : comp f1 f2 (comp f3 f4 f5 f6 f7 f8 f9 f10 f11 f12) f13 f14 -> comp f1 (comp f2 f3) f4 f5 f6 f7 f8 f9 f10 f11 (comp f12 f13) f14
+
+let step4 (x : *)
+    	  (m : id (id (id x)) -> id (id (id x)))
+	  (n : id (id (id x)) -> id (id (id x)))
+	  = focus-2-3-and-12-13
+	  (4padL (id (id (id x))))
+	  (3paddedL [id (id (id (id x)))] [m])
+	  (middlestep1 x)
+	  (middlestep2 x)
+	  (middlestep3 x)
+	  (middlestep4 x)
+	  (middlestep5 x)
+	  (I (op { 1 } (middlestep5 x)))
+	  (I (op { 1 } (middlestep4 x)))
+	  (I (op { 1 } (middlestep3 x)))
+	  (I (op { 1 } (middlestep2 x)))
+	  (I (op { 1 } (middlestep1 x)))
+	  (op { 1 } (3paddedL [id (id (id (id x)))] [n]))
+	  (op { 1 } (I (4padL (id (id (id x))))))
+
+coh sandwisk (x(f)y(g(a)h)z(k)w) : comp f g k -> comp f h k
+
+let nat-middletoleft (x : *) (y : *) (z : *) (w : *)
+    			(f1 : x -> y) (f2 : x -> y) (g1 : y -> z) (g2 : y -> z) 
+			(a : f1 -> f2) (b : g1 -> g2) (h : z -> w)
+			= sandwisk [a] b h
+
+let nat-factoring-WRT-m  (x : *)
+    	  (m : id (id (id x)) -> id (id (id x)))
+	  = nat-middletoleft (factor3padL x) (2paddedL [[id (id (id (id x)))]] [[m]] ) (I (3padL (id (id x))))
+
+let nat-factoring-WRT-n  (x : *)
+    	  (n : id (id (id x)) -> id (id (id x)))
+	  = I (nat-middletoleft (I (op { 1 } (factor3padL x))) (op { 1 } (2paddedL [[id (id (id (id x)))]] [[n]])) (I (op { 1 } (3padL (id (id x))))))
+	  
+let step5 (x : *)
+    	  (m : id (id (id x)) -> id (id (id x)))
+	  (n : id (id (id x)) -> id (id (id x)))
+	  = comp
+	  (4padL (id (id (id x))))
+	  [nat-factoring-WRT-m m]
+	  (middlestep2 x)
+	  (middlestep3 x)
+	  (middlestep4 x)
+	  (middlestep5 x)
+	  (I (op { 1 } (middlestep5 x)))
+	  (I (op { 1 } (middlestep4 x)))
+	  (I (op { 1 } (middlestep3 x)))
+	  (I (op { 1 } (middlestep2 x)))
+	  [nat-factoring-WRT-n n]
+	  (op { 1 } (I (4padL (id (id (id x))))))
+
+coh focus-3-4-and-11-12 (x0(f1)x1(f2)x2(f3)x3(f4)x4(f5)x5(f6)x6(f7)x7(f8)x8(f9)x9(f10)x10(f11)x11(f12)x12(f13)x13(f14)x14)
+    : comp f1 (comp f2 f3) f4 f5 f6 f7 f8 f9 f10 f11 (comp f12 f13) f14 -> comp f1 f2 (comp f3 f4) f5 f6 f7 f8 f9 f10 (comp f11 f12) f13 f14
+
+let step6 (x : *)
+    	  (m : id (id (id x)) -> id (id (id x)))
+	  (n : id (id (id x)) -> id (id (id x)))
+	  = focus-3-4-and-11-12
+	  (4padL (id (id (id x))))
+	  (middlestep1 x)
+	  (comp (comp (3padU x) (comp [bias x] (comp [id (id x)] [id (id x)]) [Ibias x])) [2paddedL [[id (id (id (id x)))]] [[m]]] (I (3padL (id (id x)))))
+	  (middlestep2 x)
+	  (middlestep3 x)
+	  (middlestep4 x)
+	  (middlestep5 x)
+	  (I (op { 1 } (middlestep5 x)))
+	  (I (op { 1 } (middlestep4 x)))
+	  (I (op { 1 } (middlestep3 x)))
+	  (I (op { 1 } (middlestep2 x)))
+	  (comp (op { 1 } (comp (3padU x) (comp [bias x] (comp [id (id x)] [id (id x)]) [Ibias x]))) [op { 1 } (2paddedL [[id (id (id (id x)))]] [[n]])] (I (op { 1 } (3padL (id (id x))))))
+	  (I (op { 1 } (middlestep1 x)))
+	  (op { 1 } (I (4padL (id (id (id x))))))
+
+let nat-assoc-WRT-m (x : *)
+    		    (m : id (id (id x)) -> id (id (id x)))
+		    = focus-first2-to-middle2 (3padU x) (comp [bias x] (comp [id (id x)] [id (id x)]) [Ibias x]) [2paddedL [[id (id (id (id x)))]] [[m]]] (I (3padL (id (id x))))
+
+coh focus-middle2-to-first2 (x0(f1)x1(f2)x2(f3)x3(f4)x4) : comp f1 (comp f2 f3) f4 -> comp (comp f1 f2) f3 f4
+
+let nat-assoc-WRT-n (x : *)
+    		    (n : id (id (id x)) -> id (id (id x)))
+		    = I (focus-middle2-to-first2 (3padU x) (op { 1 } (comp [bias x] (comp [id (id x)] [id (id x)]) [Ibias x])) [op { 1 } (2paddedL [[id (id (id (id x)))]] [[n]])] (I (op { 1 } (3padL (id (id x))))))
+
+let step7 (x : *)
+    	  (m : id (id (id x)) -> id (id (id x)))
+	  (n : id (id (id x)) -> id (id (id x)))
+	  = comp
+	  (4padL (id (id (id x))))
+	  (middlestep1 x)
+	  [nat-assoc-WRT-m m]
+	  (middlestep3 x)
+	  (middlestep4 x)
+	  (middlestep5 x)
+	  (I (op { 1 } (middlestep5 x)))
+	  (I (op { 1 } (middlestep4 x)))
+	  (I (op { 1 } (middlestep3 x)))
+	  [nat-assoc-WRT-n n]
+	  (I (op { 1 } (middlestep1 x)))
+	  (op { 1 } (I (4padL (id (id (id x))))))
+
+let test  (x : *)
+    	  (m : id (id (id x)) -> id (id (id x)))
+	  (n : id (id (id x)) -> id (id (id x)))
+	  = comp (step1 m n) (step2 m n) (step3 m n) (step4 m n) (step5 m n) (step6 m n) (step7 m n)
+
diff --git a/examples/eckmann-hilton-versions/higher-eh/eh430.catt b/examples/eckmann-hilton-versions/higher-eh/eh430.catt
new file mode 100644
index 00000000..0cd73335
--- /dev/null
+++ b/examples/eckmann-hilton-versions/higher-eh/eh430.catt
@@ -0,0 +1,276 @@
+let 1paddedL (x : *) (y : *)
+    	     (f : x -> x) (g : x -> y)
+	     = comp f g
+
+coh 2padL (x(f)y) : f -> 1paddedL (id x) f
+
+let 1paddedU (x : *)
+    	     (f : x -> x) (g : x -> x)
+    	     = comp f g
+
+coh 2padU (x) : id x -> 1paddedU (id x) (id x)
+
+coh bias (x) : 2padU x -> 2padL (id x)
+
+coh Ibias (x) : I (2padU x) -> I (2padL (id x))
+
+let 2paddedL (x : *) (y : *)
+    	     (f : x -> y) (g : x -> y)
+	     (a : id x -> id x) (b : f -> g)
+	     = comp (2padL f) (1paddedL [a] [b]) (I (2padL g))
+
+coh 3padL (x(f(a)g)y) : a -> 2paddedL (id (id x)) a
+
+let 2paddedU (x : *)
+    	     (a : id x -> id x) (b : id x -> id x)
+    	     = comp (2padU x) (1paddedU [a] [b]) (I (2padU x))
+
+coh 3padU (x) : id (id x) -> 2paddedU (id (id x)) (id (id x))
+
+let 3paddedL (x : *) (y : *)
+    	     (f : x -> y) (g : x -> y)
+	     (a : f -> g) (b : f -> g)
+	     (p : id (id x) -> id (id x)) (q : a -> b)
+	     = comp (3padL a) (2paddedL [p] [q]) (I (3padL b))
+	     
+coh 4padL (x(f(a(p)b)g)y) : p -> 3paddedL (id (id (id x))) p
+
+
+let 3paddedU (x : *)
+    	     (p : id (id x) -> id (id x)) (q : (id (id x)) -> (id (id x)))
+    	     = comp (3padU x) (2paddedU [p] [q]) (I (3padU x))
+
+coh 4padU (x) : id (id (id x)) -> 3paddedU (id (id (id x))) (id (id (id x)))
+
+let 4paddedL (x : *) (y : *)
+    	     (f : x -> y) (g : x -> y)
+	     (a : f -> g) (b : f -> g)
+	     (p : a -> b) (q : a -> b)
+	     (m : id (id (id x)) -> id (id (id x))) (n : p -> q)
+	     = comp (4padL p) (3paddedL [m] [n]) (I (4padL q))
+
+coh 5padL (x(f(a(p(m)q)b)g)y) : m -> 4paddedL (id (id (id (id x)))) m
+
+let 4paddedU (x : *)
+    	     (m : id (id (id x)) -> id (id (id x))) (n : id (id (id x)) -> id (id (id x)))
+	     = comp (4padU x) (3paddedU [m] [n]) (I (4padU x))
+
+coh 5padU (x) : id (id (id (id x))) -> 4paddedU (id (id (id (id x)))) (id (id (id (id x))))
+
+
+let 5paddedL (x : *) (y : *)
+    	     (f : x -> y) (g : x -> y)
+	     (a : f -> g) (b : f -> g)
+	     (p : a -> b) (q : a -> b)
+	     (m : p -> q) (n : p -> q)
+	     (A : (id (id (id (id x)))) -> id (id (id (id x)))) (B : m -> n)
+	     = comp (5padL m) (4paddedL [A] [B]) (I (5padL n))
+coh 6padL (x(f(a(p(m(A)n)q)b)g)y) : A -> 5paddedL (id (id (id (id (id x))))) A
+
+let 5paddedU (x : *)
+    	     (A : (id (id (id (id x)))) -> id (id (id (id x)))) (B : (id (id (id (id x)))) -> id (id (id (id x))))
+	     = comp (5padU x) (4paddedU [A] [B]) (I (5padU x))
+
+coh 6padU (x) : id (id (id (id (id x)))) -> 5paddedU (id (id (id (id (id x))))) (id (id (id (id (id x)))))
+
+
+
+coh factor3padL (x) : 3padL (id (id x)) -> comp (3padU x) (comp [bias x] (comp [id (id x)] [id (id x)]) [Ibias x])
+
+coh unfactor3padU (x) : comp (comp [bias x] (comp [id (id x)] [id (id x)]) [Ibias x])
+    		      	     (I (3padL (id (id x))))
+			     -> I (3padU x)
+
+coh burger (x(f(a)g)y(h)z(j(b)k)w) : comp f h j -> comp g h k
+
+let nat-of-id-WRT-bias (x : *) (y : *) (z : *) (w : *)
+    		       (f1 : x -> y) (f2 : x -> y) (g1 : y -> z) (g2 : y -> z) (h1 : z -> w) (h2 : z -> w)
+		       (a : f1 -> f2) (b : g1 -> g2) (c : h1 -> h2) 
+		       = burger a [b] c
+
+
+
+
+
+coh focus-first2-to-middle2 (x0(f1)x1(f2)x2(f3)x3(f4)x4) : comp (comp f1 f2) f3 f4 -> comp f1 (comp f2 f3) f4
+
+coh focus-middle2-to-last2 (x0(f1)x1(f2)x2(f3)x3(f4)x4) : comp f1 (comp f2 f3) f4 -> comp f1 f2 (comp f3 f4)
+
+let trapeziumcomposite (B0 : *) (B1 : *) (B2 : *) (B3 : *) (T0 : *) (T1 : *)
+    		       (b1 : B0 -> B1) (b2 : B1 -> B2) (b3 : B2 -> B3) (sL : B0 -> T0) (sR : T1 -> B3) (m1 : T0 -> B1) (m2 : T1 -> B2) (t : T0 -> T1)
+		       (fL : b1 -> comp sL m1) (fM : comp m1 b2 -> comp t m2) (fR : comp m2 b3 -> sR)
+		       = comp
+		       (comp (comp [fL] b2 b3)
+		       (focus-first2-to-middle2 sL m1 b2 b3))
+		       (comp sL [fM] b3)
+		       (comp (focus-middle2-to-last2 sL t m2 b3)
+		       (comp sL t [fR]))
+
+
+
+
+let 3paddedLto3paddedU (x : *) (p : id (id x) -> id (id x)) (q : id (id x) -> id (id x))
+    	       : 3paddedL p q -> 3paddedU p q
+    	       = trapeziumcomposite (factor3padL x) (nat-of-id-WRT-bias (bias x) (comp [[p]] [[q]]) (Ibias x)) (unfactor3padU x)
+
+let 3paddedLto3paddedU_nat  (x : *) (p0 : id (id x) -> id (id x)) (p1 : id (id x) -> id (id x)) (m : p0 -> p1) (q0 : id (id x) -> id (id x)) (q1 : id (id x) -> id (id x)) (n : q0 -> q1) = I (3paddedLto3paddedU [m] [n])
+
+let 3paddedUto3paddedR (x : *) (p : id (id x) -> id (id x)) (q : id (id x) -> id (id x))
+    		       : 3paddedU p q -> (op { 1 } (3paddedL q p))
+    		       = op { 1 } (I (3paddedLto3paddedU q p))
+
+let 3paddedUto3paddedR_nat  (x : *) (p0 : id (id x) -> id (id x)) (p1 : id (id x) -> id (id x)) (m : p0 -> p1) (q0 : id (id x) -> id (id x)) (q1 : id (id x) -> id (id x)) (n : q0 -> q1) = 3paddedUto3paddedR [m] [n]
+
+
+
+
+
+let middlehalf (x : *)
+    	       = 3paddedLto3paddedU (id (id (id x))) (id (id (id x)))
+
+let middle (x : *) = comp (middlehalf x) (op { 1 } (I (middlehalf x)))
+
+coh middlereplace (x) : comp (I (4padL (id (id (id x))))) (op { 1 } (4padL (id (id (id x))))) -> middle x
+
+
+
+
+
+
+
+coh whiskering_interchange (x(f)y(g(a)h(b)i)z(k)w) : comp (comp f [a] k) (comp f [b] k) -> comp f [comp a b] k
+
+coh whiskering_interchange+ (x(f)y(g(a(p)b(q)c)h)z(k)w) : comp (comp f [[p]] k) (comp f [[q]] k) -> comp f [[comp p q]] k
+
+let interchange1 (x : *) (m : id (id (id x)) -> id (id (id x)))  (n : id (id (id x)) -> id (id (id x)))
+    		 = whiskering_interchange (3padU x) (2paddedU [[id (id (id (id x)))]] [[m]]) (2paddedU [[n]] [[id (id (id (id x)))]]) (I (3padU x))
+
+let interchange2 (x : *) (m : id (id (id x)) -> id (id (id x)))  (n : id (id (id x)) -> id (id (id x)))
+    		 = comp (3padU x) [[whiskering_interchange+ (2padU x) (comp [[[id (id (id (id x)))]]] [[[m]]]) (comp [[[n]]] [[[id (id (id (id x)))]]]) (I (2padU x))]] (I (3padU x))
+
+coh interchange_inside (x(f(a(p(A)q)b)g)y(h(c(r(B)s)d)i)z) : comp (comp [[[id p]]] [[[B]]]) (comp [[[A]]] [[[id s]]]) -> comp [[[A]]] [[[B]]]
+
+let interchange3 (x : *) (m : id (id (id x)) -> id (id (id x)))  (n : id (id (id x)) -> id (id (id x)))
+    		 = comp (3padU x) [[comp (2padU x) [[[interchange_inside n m]]] (I (2padU x))]] (I (3padU x))
+
+let interchange (x : *) (m : id (id (id x)) -> id (id (id x))) (n : id (id (id x)) -> id (id (id x)))
+    		 = comp (interchange1 m n) (interchange2 m n) (interchange3 m n)
+
+
+
+
+
+coh tidyl (x) : comp (4padL (id (id (id x)))) (3paddedLto3paddedU (id (id (id x))) (id (id (id x)))) -> 4padU x
+
+coh tidyr (x) : comp (3paddedUto3paddedR (id (id (id x))) (id (id (id x)))) (I (op { 1 } (4padL (id (id (id x)))))) -> I (4padU x)
+
+
+
+
+
+coh focus-33-to-middle2 (x0(f1)x1(f2)x2(f3)x3(f4)x4(f5)x5(f6)x6) :
+    comp (comp f1 f2 f3) (comp f4 f5 f6) -> comp f1 f2 (comp f3 f4) f5 f6
+
+coh focus-middle2-to-1221 (x0(f1)x1(f2)x2(f3)x3(f4)x4(f5)x5(f6)x6) : comp f1 f2 (comp f3 f4) f5 f6 -> comp f1 (comp f2 f3) (comp f4 f5) f6
+
+coh focus-1221-to-222 (x0(f1)x1(f2)x2(f3)x3(f4)x4(f5)x5(f6)x6) : comp f1 (comp f2 f3) (comp f4 f5) f6 -> comp (comp f1 f2) (comp f3 f4) (comp f5 f6)
+
+let totalshape (A0 : *) (B0 : *) (C0 : *)
+    	       	     	(B1 : *) 
+    	       (A1 : *)	      	 (C1 : *)
+			(B2 : *)
+	       (A2 : *) (B3 : *) (C2 : *)
+
+	       (m : A0 -> A1) (n : A1 -> A2)
+	       (lpad : A0 -> B0) (lwhiskm : B0 -> B1) (ilpad : B1 -> A1) (rpad : A1 -> B2) (rwhiskn : B2 -> B3) (irpad : B3 -> A2)
+	       (lmoves_outer : B0 -> C0) (lmoves_inner : B1 -> C1) (rmoves_inner : C1 -> B2) (rmoves_outer : C2 -> B3)
+	       (uwhiskm : C0 -> C1) (uwhiskn : C1 -> C2) (mn : C0 -> C2) (upad : A0 -> C0) (iupad : C2 -> A2)
+
+	       (lpadm : m -> comp lpad lwhiskm ilpad) (rpadn : n -> comp rpad rwhiskn irpad)
+	       (middlereplace : comp ilpad rpad -> comp lmoves_inner rmoves_inner)
+	       (lnat : comp lwhiskm lmoves_inner -> comp lmoves_outer uwhiskm)
+	       (rnat : comp rmoves_inner rwhiskn -> comp uwhiskn rmoves_outer)
+	       (interchange : comp uwhiskm uwhiskn -> mn) (tidyl : comp lpad lmoves_outer -> upad) (tidyr : comp rmoves_outer irpad -> iupad)
+
+	       = comp
+	       (comp [lpadm] [rpadn])
+	       (focus-33-to-middle2 _ _ _ _ _ _)
+	       (comp _ _ [middlereplace] _ _)
+	       (focus-middle2-to-1221 _ _ _ _ _ _)
+	       (comp _ [lnat] [rnat] _)
+	       (focus-1221-to-222 _ _ _ _ _ _)
+	       (comp [tidyl] [interchange] [tidyr])
+
+
+
+let eh430 (x : *) (m : id (id (id x)) -> id (id (id x))) (n : id (id (id x)) -> id (id (id x)))
+    	  : comp m n -> 4paddedU n m
+    	  = totalshape
+	  (5padL m) (op { 1 } (5padL n))
+	  (middlereplace x)
+	  (3paddedLto3paddedU_nat (id (id (id (id x)))) m)
+	  (3paddedUto3paddedR_nat n (id (id (id (id x)))))
+	  (interchange m n)
+	  (tidyl x) (tidyr x)
+
+coh factor4padL (x) : 4padL (id (id (id x))) -> comp (4padU x) (I (3paddedLto3paddedU (id (id (id x))) (id (id (id x)))))
+
+let 3paddedUto3paddedL (x : *) (a : id (id x) -> id (id x)) (b : id (id x) -> id (id x)) = I (3paddedLto3paddedU a b)
+
+let 3paddedUto3paddedL_nat (x : *) (a0 : id (id x) -> id (id x)) (a1 : id (id x) -> id (id x)) (a : a0 -> a1) (b0 : id (id x) -> id (id x)) (b1 : id (id x) -> id (id x)) (b : b0 -> b1) = 3paddedUto3paddedL [a] [b]
+
+coh unfactor4padU (x) : comp (3paddedUto3paddedL (id (id (id x))) (id (id (id x)))) (I (4padL (id (id (id x))))) -> I (4padU x) 
+
+let 4paddedLto4paddedU (x : *) (a : (id (id (id x))) -> (id (id (id x))))
+    : 4paddedL (id (id (id (id x)))) a -> 4paddedU (id (id (id (id x)))) a
+    = trapeziumcomposite (factor4padL x) (3paddedUto3paddedL_nat (id (id (id (id x)))) a) (unfactor4padU x)
+
+let 4paddedLto4paddedU_nat (x : *) (a0 : (id (id (id x))) -> (id (id (id x)))) (a1 : (id (id (id x))) -> (id (id (id x)))) (a : a0 -> a1)
+
+    = 4paddedLto4paddedU [a]
+
+
+let 4paddedUto4paddedR (x : *) (a : (id (id (id x))) -> (id (id (id x))))
+    = I (op { 1 } (4paddedLto4paddedU a))
+
+let 4paddedUto4paddedR_nat (x : *) (a0 : (id (id (id x))) -> (id (id (id x)))) (a1 : (id (id (id x))) -> (id (id (id x)))) (a : a0 -> a1)
+
+    = 4paddedUto4paddedR [a]
+
+coh middlereplace+ (x) : comp (I (5padL (id (id (id (id x)))))) (op { 1 } (5padL (id (id (id (id x)))))) -> comp (4paddedLto4paddedU (id (id (id (id x))))) (4paddedUto4paddedR (id (id (id (id x)))))
+
+
+coh whiskering_interchange++ (x(f)y(g(a(p(A)q(B)r)b)h)z(k)w) : comp (comp f [[[A]]] k) (comp f [[[B]]] k) -> comp f [[[comp A B]]] k
+
+let interchange+1 (x : *) (a : id (id (id (id x))) -> id (id (id (id x))))  (b : id (id (id (id x))) -> id (id (id (id x))))
+    = whiskering_interchange (4padU x) (3paddedU [[id (id (id (id (id x))))]] [[a]]) (3paddedU [[b]] [[id (id (id (id (id x))))]]) (I (4padU x))
+
+
+let interchange+2 (x : *) (a : id (id (id (id x))) -> id (id (id (id x))))  (b : id (id (id (id x))) -> id (id (id (id x))))
+    = comp (4padU x) [[whiskering_interchange+ (3padU x) (2paddedU [[[id (id (id (id (id x))))]]] [[[a]]]) (2paddedU [[[b]]] [[[id (id (id (id (id x))))]]]) (I (3padU x))]] (I (4padU x))
+
+let interchange+3 (x : *) (a : id (id (id (id x))) -> id (id (id (id x))))  (b : id (id (id (id x))) -> id (id (id (id x))))
+    = comp (4padU x) [[comp (3padU x) [[[whiskering_interchange++ (2padU x) (1paddedU [[[[id (id (id (id (id x))))]]]] [[[[a]]]]) (1paddedU [[[[b]]]] [[[[id (id (id (id (id x))))]]]]) (I (2padU x))]]] (I (3padU x))]] (I (4padU x))
+
+coh interchange_inside+ (x(f(a(p(A(S)B)q)b)g)y(h(c(r(C(T)D)s)d)i)z) : comp (comp [[[[id A]]]] [[[[T]]]]) (comp [[[[S]]]] [[[[id D]]]]) -> comp [[[[S]]]] [[[[T]]]]
+
+let interchange+ (x : *) (a : id (id (id (id x))) -> id (id (id (id x))))  (b : id (id (id (id x))) -> id (id (id (id x))))
+ = comp
+ (interchange+1 a b)
+ (interchange+2 a b)
+ (interchange+3 a b)
+ (comp (4padU x) [[comp (3padU x) [[[comp (2padU x) [[[[interchange_inside+ b a]]]] (I (2padU x))]]] (I (3padU x))]] (I (4padU x)))
+
+coh tidyl+ (x) : comp (5padL (id (id (id (id x))))) (4paddedLto4paddedU (id (id (id (id x))))) -> 5padU x
+
+coh tidyr+ (x) : comp (4paddedUto4paddedR (id (id (id (id x))))) (I (op { 1 } (5padL (id (id (id (id x))))))) -> I (5padU x)
+
+let eh540 (x : *) (a : id (id (id (id x))) -> id (id (id (id x)))) (b : id (id (id (id x))) -> id (id (id (id x))))
+    	  : comp a b -> 5paddedU b a
+    	  = totalshape
+	  (6padL a) (op { 1 } (6padL b))
+	  (middlereplace+ x)
+	  (4paddedLto4paddedU_nat a)
+	  (4paddedUto4paddedR_nat b)
+	  (interchange+ a b)
+	  (tidyl+ x) (tidyr+ x)
diff --git a/examples/eckmann-hilton-versions/higher-eh/ehbasecases.catt b/examples/eckmann-hilton-versions/higher-eh/ehbasecases.catt
new file mode 100644
index 00000000..22069f46
--- /dev/null
+++ b/examples/eckmann-hilton-versions/higher-eh/ehbasecases.catt
@@ -0,0 +1,185 @@
+let padded1 (x : *) (p : x -> x) = p
+let bpadded1 (x : *) (y : *) (q : x -> y) = q
+
+coh pad1 (x) : id x -> padded1 (comp (id x) (id x))
+coh bpad1 (x(f)y) : f -> bpadded1 (comp f (id y))
+
+let padded2 (x : *) (p : comp (id x) (id x) -> comp (id x) (id x))
+    = comp (pad1 x) (padded1 [p]) (I (pad1 x))
+let bpadded2 (x : *) (y : *) (f : x -> y) (g : x -> y) (q : comp f (id y) -> comp g (id y))
+    = comp (bpad1 f) (bpadded1 [q]) (I (bpad1 g))
+
+coh pad2 (x) : id (id x) -> padded2 (comp [id (id x)] [id (id x)])
+coh bpad2 (x(f(a)g)y) : a -> bpadded2 (comp [a] [id (id y)])
+
+let padded3 (x : *) (p : comp [id (id x)] [id (id x)] -> comp [id (id x)] [id (id x)])
+    = comp (pad2 x) (padded2 [p]) (I (pad2 x))
+let bpadded3 (x : *) (y : *) (f : x -> y) (g : x -> y) (a : f -> g) (b : f -> g) (q : comp [a] [id (id y)] -> comp [b] [id (id y)])
+    = comp (bpad2 a) (bpadded2 [q]) (I (bpad2 b))
+
+coh pad3 (x) : id (id (id x)) -> padded3 (comp [[id (id (id x))]] [[id (id (id x))]])
+coh bpad3 (x(f(a(X)b)g)y) : X -> bpadded3 (comp [[X]] [[id (id (id y))]])
+
+let padded4 (x : *) (p : comp [[id (id (id x))]] [[id  (id (id x))]] -> comp [[id (id (id x))]] [[id  (id (id x))]])
+    = comp (pad3 x) (padded3 [p]) (I (pad3 x))
+let bpadded4 (x : *) (y : *) (f : x -> y) (g : x -> y) (a : f -> g) (b : f -> g) (X : a -> b) (Y : a -> b) (q : comp [[X]] [[id (id (id y))]] -> comp [[Y]] [[id (id (id y))]])
+    = comp (bpad3 X) (bpadded3 [q]) (I (bpad3 Y))
+
+coh pad4 (x) : id (id (id (id x))) -> padded4 (comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]])
+coh bpad4 (x(f(a(X(F)Y)b)g)y) : F -> bpadded4 (comp [[[F]]] [[[id (id (id (id y)))]]])
+
+let padded5 (x : *) (p : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]])
+    = comp (pad4 x) (padded4 [p]) (I (pad4 x))
+let bpadded5 (x : *) (y : *) (f : x -> y) (g : x -> y) (a : f -> g) (b : f -> g) (X : a -> b) (Y : a -> b) (F : X -> Y) (G : X -> Y) (q : comp [[[F]]] [[[id (id (id (id y)))]]] -> comp [[[G]]] [[[id (id (id (id y)))]]])
+    = comp (bpad4 F) (bpadded4 [q]) (I (bpad4 G))
+
+coh pad5 (x) : id (id (id (id (id x)))) -> padded5 (comp [[[[id (id (id (id (id x))))]]]] [[[[id (id (id (id (id x))))]]]])
+coh bpad5 (x(f(a(X(F(A)G)Y)b)g)y) : A -> bpadded5 (comp [[[[A]]]] [[[[id (id (id (id (id y))))]]]])
+
+
+
+
+
+
+
+coh peel1 (x(f)y(g(a)h(b)i)z(j)w) : comp (comp f [a] j) (comp f [b] j) -> comp f [comp a b] j
+coh peel2 (x(f)y(g(a(X)b(Y)c)h)z(j)w) : comp (comp f [[X]] j) (comp f [[Y]] j) -> comp f [[comp X Y]] j
+coh peel3 (x(f)y(g(a(X(F)Y(G)Z)b)h)z(j)w) : comp (comp f [[[F]]] j) (comp f [[[G]]] j) -> comp f [[[comp F G]]] j
+
+let collapse3 (x : *) (p : comp [id (id x)] [id (id x)] -> comp [id (id x)] [id (id x)]) (q : comp [id (id x)] [id (id x)] -> comp [id (id x)] [id (id x)])
+    = peel1 (pad1 x) p q (I (pad1 x))
+
+coh interchange3 (x(f(a(X)b)g)y(h(c(Y)d)i)z) : comp (comp [[X]] [[id c]]) (comp [[id b]] [[Y]]) -> comp [[X]] [[Y]]
+
+let move_parallel3 (x : *) (a : id (id x) -> id (id x)) (b : id (id x) -> id (id x))
+    = comp (collapse3 (comp [[a]] [[id (id (id x))]]) (comp [[id (id (id x))]] [[b]])) (padded2 [[interchange3 a b]])
+
+
+coh interchange4 (x(f(a(X(F)Y)b)g)y(h(c(Z(G)W)d)i)z) : comp (comp [[[F]]] [[[id Z]]]) (comp [[[id Y]]] [[[G]]]) -> comp [[[F]]] [[[G]]]
+
+
+
+
+coh focus33tomiddle2 (x0(f1)x1(f2)x2(f3)x3(f4)x4(f5)x5(f6)x6) : comp (comp f1 f2 f3) (comp f4 f5 f6) -> comp f1 f2 (comp f3 f4) f5 f6
+
+coh 4unitor (x0(f1)x1(f2)x2(f3)x3(f4)x4) : comp f1 f2 (id x2) f3 f4 -> comp f1 (comp f2 f3) f4
+
+let collapse12 (x : *) (p : comp [id (id x)] [id (id x)] -> comp [id (id x)] [id (id x)]) (q : comp [id (id x)] [id (id x)] -> comp [id (id x)] [id (id x)])
+    : comp (padded1 [[p]]) (padded1 [[q]]) -> padded1 [[comp p q]]
+    = id (comp p q)
+
+let collapse21 (x : *) (p : comp [id (id x)] [id (id x)] -> comp [id (id x)] [id (id x)]) (q : comp [id (id x)] [id (id x)] -> comp [id (id x)] [id (id x)])
+    : comp (padded2 [p]) (padded2 [q]) -> padded2 [comp p q]
+    = comp (peel1 (pad1 x) (padded1 [[p]]) (padded1 [[q]]) (I (pad1 x))) (comp _ [[collapse12 p q]] _)
+
+let collapse30 (x : *) (p : comp [id (id x)] [id (id x)] -> comp [id (id x)] [id (id x)]) (q : comp [id (id x)] [id (id x)] -> comp [id (id x)] [id (id x)])
+    : comp (padded3 p) (padded3 q) -> padded3 (comp p q)
+    = comp
+    (focus33tomiddle2 (pad2 x) (padded2 [p]) (I (pad2 x)) (pad2 x) (padded2 [q]) (I (pad2 x)))
+    (comp _ _ [U (I (pad2 x))] _ _)
+    (4unitor (pad2 x) (padded2 [p]) (padded2 [q]) (I (pad2 x)))
+    (comp _ [collapse21 p q] _)
+
+let collapse13 (x : *) (p : comp [[id (id (id x))]] [[id (id (id x))]] -> comp [[id (id (id x))]] [[id (id (id x))]]) (q : comp [[id (id (id x))]] [[id (id (id x))]] -> comp [[id (id (id x))]] [[id (id (id x))]])
+    : comp (padded1 [[[p]]]) (padded1 [[[q]]]) -> padded1 [[[comp p q]]]
+    = id (comp p q)
+
+let collapse22 (x : *) (p : comp [[id (id (id x))]] [[id (id (id x))]] -> comp [[id (id (id x))]] [[id (id (id x))]]) (q : comp [[id (id (id x))]] [[id (id (id x))]] -> comp [[id (id (id x))]] [[id (id (id x))]])
+    : comp (padded2 [[p]]) (padded2 [[q]]) -> padded2 [[comp p q]]
+    = comp
+    (peel2 (pad1 x) (padded1 [[[p]]]) (padded1 [[[q]]]) (I (pad1 x))) (comp _ [[[collapse13 p q]]] _)
+
+let collapse31 (x : *) (p : comp [[id (id (id x))]] [[id (id (id x))]] -> comp [[id (id (id x))]] [[id (id (id x))]]) (q : comp [[id (id (id x))]] [[id (id (id x))]] -> comp [[id (id (id x))]] [[id (id (id x))]])
+    : comp (padded3 [p]) (padded3 [q]) -> padded3 [comp p q]
+    = comp (peel1 (pad2 x) (padded2 [[p]]) (padded2 [[q]]) (I (pad2 x))) (comp _ [[collapse22 p q]] _)
+
+let collapse40 (x : *) (p : comp [[id (id (id x))]] [[id (id (id x))]] -> comp [[id (id (id x))]] [[id (id (id x))]]) (q : comp [[id (id (id x))]] [[id (id (id x))]] -> comp [[id (id (id x))]] [[id (id (id x))]])
+    : comp (padded4 p) (padded4 q) -> padded4 (comp p q)
+    = comp
+    (focus33tomiddle2 (pad3 x) (padded3 [p]) (I (pad3 x)) (pad3 x) (padded3 [q]) (I (pad3 x)))
+    (comp _ _ [U (I (pad3 x))] _ _)
+    (4unitor (pad3 x) (padded3 [p]) (padded3 [q]) (I (pad3 x)))
+    (comp _ [collapse31 p q] _)
+
+let collapse14 (x : *) (p : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]]) (q : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]])
+    : comp (padded1 [[[[p]]]]) (padded1 [[[[q]]]]) -> padded1 [[[[comp p q]]]]
+    = id (comp p q)
+
+let collapse23 (x : *) (p : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]]) (q : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]])
+    : comp (padded2 [[[p]]]) (padded2 [[[q]]]) -> padded2 [[[comp p q]]]
+    = comp (peel3 (pad1 x) (padded1 [[[[p]]]]) (padded1 [[[[q]]]]) (I (pad1 x))) (comp _ [[[[collapse14 p q]]]] _)
+
+let collapse32 (x : *) (p : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]]) (q : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]])
+    : comp (padded3 [[p]]) (padded3 [[q]]) -> padded3 [[comp p q]]
+    = comp (peel2 (pad2 x) (padded2 [[[p]]]) (padded2 [[[q]]]) (I (pad2 x))) (comp _ [[[collapse23 p q]]] _)
+
+let collapse41 (x : *) (p : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]]) (q : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]])
+    : comp (padded4 [p]) (padded4 [q]) -> padded4 [comp p q]
+    = comp (peel1 (pad3 x) (padded3 [[p]]) (padded3 [[q]]) (I (pad3 x))) (comp _ [[collapse32 p q]] _)
+
+let collapse50 (x : *) (p : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]]) (q : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]])
+    : comp (padded5 p) (padded5 q) -> padded5 (comp p q)
+    = comp
+    (focus33tomiddle2 (pad4 x) (padded4 [p]) (I (pad4 x)) (pad4 x) (padded4 [q]) (I (pad4 x)))
+    (comp _ _ [U (I (pad4 x))] _ _)
+    (4unitor (pad4 x) (padded4 [p]) (padded4 [q]) (I (pad4 x)))
+    (comp _ [collapse41 p q] _)
+
+coh interchange5 (x(f(a(X(F(A)G)Y)b)g)y(h(c(Z(H(B)K)W)d)i)z) : comp (comp [[[[A]]]] [[[[id H]]]]) (comp [[[[id G]]]] [[[[B]]]]) -> comp [[[[A]]]] [[[[B]]]]
+
+let hexcomp (x : *) (y- : *) (y+ : *) (y> : y- -> y+) (z- : *) (z+ : *) (z> : z- -> z+) (w : *) (f- : x -> y-) (f+ : x -> y+) (f> : comp f- y> -> f+) (g- : y- -> z-) (g+ : y+ -> z+) (g> : comp g- z> -> comp y> g+) (h- : z- -> w) (h+ : z+ -> w) (h> : h- -> comp z> h+)
+    = @comp _ [_] [f>] [_] [g>] _ [h>]
+
+let unbias1 (x : *) (p : x -> x) : bpadded1 p -> padded1 p
+    = id p
+coh factor1 (x) :  I (bpad1 (id x)) -> comp (unbias1 (comp (id x) (id x))) (I (pad1 x))
+coh unfactor1 (x) : comp (bpad1 (id x)) (unbias1 (comp (id x) (id x))) -> pad1 x
+
+let unbias2 (x : *) (p : comp (id x) (id x) -> comp (id x) (id x)) : bpadded2 p -> padded2 p
+    = hexcomp (unfactor1 x) (I (unbias1 [p])) (factor1 x)
+coh factor2 (x) : I (bpad2 (id (id x))) -> comp (unbias2 (comp [id (id x)] [id (id x)])) (I (pad2 x))
+coh unfactor2 (x) : comp (bpad2 (id (id x))) (unbias2 (comp [id (id x)] [id (id x)])) -> pad2 x
+
+let unbias3 (x : *) (p : comp [id (id x)] [id (id x)] -> comp [id (id x)] [id (id x)]) : bpadded3 p -> padded3 p
+    = hexcomp (unfactor2 x) (I (unbias2 [p])) (factor2 x)
+coh factor3 (x) : I (bpad3 (id (id (id x)))) -> comp (unbias3 (comp [[id (id (id x))]] [[id (id (id x))]])) (I (pad3 x))
+coh unfactor3 (x) : comp (bpad3 (id (id (id x)))) (unbias3 (comp [[id (id (id x))]] [[id (id (id x))]])) -> pad3 x
+
+let upad3 (x : *) (a : id (id x) -> id (id x))
+    = comp (bpad3 a) (unbias3 (comp [[a]] [[id (id (id x))]]))
+
+let eh320 (x : *) (a : id (id x) -> id (id x)) (b : id (id x) -> id (id x))
+    : comp a b -> padded3 (comp [[a]] [[b]])
+    = comp
+    (comp [upad3 a] [op { 1 } (upad3 b)])
+    (collapse30 (comp [[a]] [[id (id (id x))]]) (comp [[id (id (id x))]] [[b]]))
+    (padded3 [interchange3 a b])
+    
+let unbias4 (x : *) (p : comp [[id (id (id x))]] [[id (id (id x))]] -> comp [[id (id (id x))]] [[id (id (id x))]]) : bpadded4 p -> padded4 p
+    = hexcomp (unfactor3 x) (I (unbias3 [p])) (factor3 x)
+coh factor4 (x) : I (bpad4 (id (id (id (id x))))) -> comp (unbias4 (comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]])) (I (pad4 x))
+coh unfactor4 (x) : comp (bpad4 (id (id (id (id x))))) (unbias4 (comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]])) -> pad4 x
+
+
+let upad4 (x : *) (a : id (id (id x)) -> id (id (id x)))
+    = comp (bpad4 a) (unbias4 (comp [[[a]]] [[[id (id (id (id x)))]]]))
+
+let eh430 (x : *) (a : id (id (id x)) -> id (id (id x))) (b : id (id (id x)) -> id (id (id x)))
+    : comp a b -> padded4 (comp [[[a]]] [[[b]]])
+    = comp
+    (comp [upad4 a] [op { 1 } (upad4 b)])
+    (collapse40 (comp [[[a]]] [[[id (id (id (id x)))]]]) (comp [[[id (id (id (id x)))]]] [[[b]]]))
+    (padded4 [interchange4 a b])
+
+let unbias5 (x : *) (p : comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]] -> comp [[[id (id (id (id x)))]]] [[[id (id (id (id x)))]]]) : bpadded5 p -> padded5 p
+    = hexcomp (unfactor4 x) (I (unbias4 [p])) (factor4 x)
+    
+let upad5 (x : *) (a : id (id (id (id x))) -> id (id (id (id x))))
+    = comp (bpad5 a) (unbias5 (comp [[[[a]]]] [[[[id (id (id (id (id x))))]]]]))
+
+let eh540 (x : *) (a : id (id (id (id x))) -> id (id (id (id x)))) (b : id (id (id (id x))) -> id (id (id (id x))))
+    : comp a b -> padded5 (comp [[[[a]]]] [[[[b]]]])
+    = comp
+    (comp [upad5 a] [op { 1 } (upad5 b)])
+    (collapse50 (comp [[[[a]]]] [[[[id (id (id (id (id x))))]]]]) (comp [[[[id (id (id (id (id x))))]]]] [[[[b]]]]))
+    (padded5 [interchange5 a b])
diff --git a/examples/eh-builtin.catt b/examples/eh-builtin.catt
new file mode 100644
index 00000000..1f4c8d01
--- /dev/null
+++ b/examples/eh-builtin.catt
@@ -0,0 +1,16 @@
+check eh(2,0,1)
+check eh(3,0,1)
+check eh(4,2,1)
+check eh(3,1,2)
+check eh(4,3,2)
+check eh(3,1,2)
+check eh(4,2,3)
+check eh(3,0,2)
+check eh(2,1,0)
+check eh(9,8,7)
+check eh(3,2,0)
+check EH(2,0,1)
+check EH(3,0,1)
+check EH(3,1,2)
+check EH(3,1,2)
+check EH(3,2,0)
diff --git a/examples/horizontalinverses.catt b/examples/horizontalinverses.catt
new file mode 100644
index 00000000..47c43d86
--- /dev/null
+++ b/examples/horizontalinverses.catt
@@ -0,0 +1,15 @@
+coh unit_l (x(f)y) : f -> comp (id x) f
+
+coh unit_r (x(f)y) : f -> comp f (id y)
+
+coh h_unit_l (x(f(a)g)y) : a -> comp (unit_l f) (commp [id (id x)] [a]) (I(unit_l g))
+
+let v_inverse (x : *) (y : *) (f : x -> y) (g : x -> y) (if : y -> x) (ig : y -> x) (ef : id x -> comp f if) (ieig : comp ig g -> id y) (ia : if -> ig)
+=
+comp (unit_l g) (comp [ef] g) (comp f [ia] g) (comp f [ieig]) (I (unit_r f))
+
+let v_witness (x : *) (y : *) (f : x -> y) (g : x -> y) (if : y -> x) (ig : y -> x) (ef : id x -> comp f if) (ief : comp f if -> f) (eef : id (id x) -> comp ef ief) (ieg : comp g ig -> id x) (ieig : comp ig g -> id y) (a : f -> g) (ia : if -> ig) (ea: comp (ef) (comp [a] [ia]) (ieg) -> id (id x))
+: comp a (v_inverse ef ieig ia) a -> id f
+= comp
+(comp [h_unit_l a] (v_inverse ef ieig ia))
+
diff --git a/lib/eh.ml b/lib/eh.ml
new file mode 100644
index 00000000..84fc72b0
--- /dev/null
+++ b/lib/eh.ml
@@ -0,0 +1,608 @@
+open Common
+open Kernel
+open Unchecked_types.Unchecked_types (Coh) (Tm)
+
+module type EHArgsS = sig
+  val n : int
+  val k : int
+  val l : int
+end
+
+module type BiasedPaddingArgsS = sig
+  val n : int
+end
+
+let memo_nkl = Hashtbl.create 97
+let memo_n = Hashtbl.create 97
+
+let nkl_module n k l =
+  match Hashtbl.find_opt memo_nkl (n, k, l) with
+  | Some m -> m
+  | None ->
+      let res =
+        (module struct
+          let n = n
+          let k = k
+          let l = l
+        end : EHArgsS)
+      in
+      Hashtbl.add memo_nkl (n, k, l) res;
+      res
+
+let n_module n =
+  match Hashtbl.find_opt memo_n n with
+  | Some m -> m
+  | None ->
+      let res =
+        (module struct
+          let n = n
+        end : BiasedPaddingArgsS)
+      in
+      Hashtbl.add memo_n n res;
+      res
+
+module UnbiasedPadding (NKL : EHArgsS) = Padding.Padding.MakeCanonical (struct
+  let name = "UBPad"
+  let x = Var.Db 0
+  let x_constr = (Var x, Obj)
+
+  let id2 i j =
+    let id = Construct.id_n i (Var x, Obj) in
+    if j < i then Construct.wcomp id j id else id
+
+  let id_l_id i = id2 i NKL.l
+
+  module F = Padding.Filtration.Make (struct
+    let min = Int.min NKL.k NKL.l + 1
+    let max = NKL.n
+    let v _ = Var.Db 1
+    let ty i = Construct.arr (id_l_id i) (id_l_id i)
+    let ctx i = [ (v i, (ty (i - 1), true)); (x, (Obj, false)) ]
+  end)
+
+  module D = struct
+    let ps _ = Unchecked.disc 0
+    let p_src i = id2 i NKL.k
+    let q_tgt i = id2 i NKL.k
+    let p_inc _ = [ x_constr ]
+    let q_inc _ = [ x_constr ]
+
+    let pad_in_ps i =
+      [ (F.v i, (Construct.to_tm (id_l_id i), true)); (x, (Var x, false)) ]
+  end
+end)
+
+let t_comp_id d t x = if d = 0 then t else Construct.(wcomp t 0 (id_n d x))
+
+module ForwardBiasedPadding (N : BiasedPaddingArgsS) =
+Padding.Padding.MakeCanonical (struct
+  let name = "FPad"
+
+  module F = Padding.Filtration.Make (struct
+    let min = 1
+    let max = N.n
+    let ctx i = Unchecked.ps_to_ctx (Unchecked.disc i)
+    let v i = Var.Db (2 * i)
+  end)
+
+  module D = struct
+    let ps i = Unchecked.disc i
+    let p_src i = t_comp_id i (F.src_v (i + 1)) (Var (Var.Db 1), Obj)
+    let q_tgt i = p_src i
+    let p_inc i = [ (Var (Var.Db (2 * i)), Unchecked.disc_type i) ]
+    let q_inc i = [ (Var (Var.Db ((2 * i) + 1)), Unchecked.disc_type i) ]
+    let pad_in_ps i = Unchecked.(identity (ps_to_ctx (ps i)))
+  end
+end)
+
+module BackwardBiasedPadding (N : BiasedPaddingArgsS) =
+Padding.Padding.MakeCanonical (struct
+  let d_src i = (Var (Var.Db (2 * i)), Unchecked.disc_type i)
+  let d_tgt i = (Var (Var.Db ((2 * i) + 1)), Unchecked.disc_type i)
+  let name = "BPad"
+
+  module F = Padding.Filtration.Make (struct
+    let min = 1
+    let max = N.n
+
+    let ty_v i =
+      Construct.arr
+        (t_comp_id i (d_src i) (d_tgt 0))
+        (t_comp_id i (d_tgt i) (d_tgt 0))
+
+    let v i = Var.Db (2 * i)
+    let ctx i = (v i, (ty_v (i - 1), true)) :: Unchecked.sphere (i - 1)
+  end)
+
+  module D = struct
+    let ps i = Unchecked.disc i
+    let p_src i = d_src i
+    let q_tgt i = d_src i
+    let p_inc i = [ d_src i ]
+    let q_inc i = [ d_tgt i ]
+
+    let pad_in_ps i =
+      (F.v i, (Construct.to_tm (F.src_v (i + 1)), true))
+      :: Unchecked.(identity (sphere (i - 1)))
+  end
+end)
+
+module ForwardToUnbiasedRepadding (N : BiasedPaddingArgsS) =
+Padding.Repadding.MakeCanonical (struct
+  let name = "FToURepad"
+
+  module NKL = (val nkl_module N.n 0 (N.n - 1) : EHArgsS)
+  module P2 = UnbiasedPadding (NKL)
+  module FP = ForwardBiasedPadding (N)
+
+  module M : Padding.FiltrationMorphismS = struct
+    let name = "id"
+
+    let sub i =
+      Unchecked.sub_ps_to_sub
+        (Construct.characteristic_sub_ps (P2.F.v_constr i))
+  end
+
+  module P1 = Padding.PaddingApp (P2.F) (M) (FP)
+
+  module D = struct
+    let ps _ = Br []
+    let incl _ = [ (Var (Var.Db 0), Obj) ]
+  end
+end)
+
+module BackwardToUnbiasedRepadding (N : BiasedPaddingArgsS) =
+Padding.Repadding.MakeCanonical (struct
+  let name = "BToURepad"
+
+  module NKL = (val nkl_module N.n (N.n - 1) 0)
+  module P2 = UnbiasedPadding (NKL)
+  module BP = BackwardBiasedPadding (N)
+
+  module M : Padding.FiltrationMorphismS = struct
+    let name = "id"
+
+    let sub i =
+      let id_pt i = Construct.(to_tm (id_n i (Var (Var.Db 0), Obj))) in
+      let rec sphere_to_point i =
+        match i with
+        | -1 -> []
+        | i ->
+            (Var.Db ((2 * i) + 1), (id_pt i, false))
+            :: (Var.Db (2 * i), (id_pt i, false))
+            :: sphere_to_point (i - 1)
+      in
+      (BP.F.v i, (Var (P2.F.v i), true)) :: sphere_to_point (i - 1)
+  end
+
+  module P1 = Padding.PaddingApp (P2.F) (M) (BP)
+
+  module D = struct
+    let ps _ = Br []
+    let incl _ = [ (Var (Var.Db 0), Obj) ]
+  end
+end)
+
+module SuspUnbiasedToUnbiasedRepadding (NKL : EHArgsS) =
+Padding.Repadding.MakeCanonical (struct
+  let name = "SuspUToURepad"
+
+  module PrevNKL = (val nkl_module (NKL.n - 1) (NKL.k - 1) (NKL.l - 1))
+
+  let x = Var.Db 0
+  let x_constr = (Var x, Obj)
+
+  module P2 = UnbiasedPadding (NKL)
+  module Prev = Padding.Suspend (UnbiasedPadding (PrevNKL))
+
+  module M : Padding.FiltrationMorphismS = struct
+    let name = "Susp"
+
+    let sub _ =
+      let list = [ P2.v_constr; Construct.id x_constr; x_constr; x_constr ] in
+      Construct.make_sub Prev.ctx list
+  end
+
+  module P1 = Padding.PaddingApp (P2.F) (M) (Prev)
+
+  module D = struct
+    let ps _ = Br []
+    let incl _ = [ x_constr ]
+  end
+end)
+
+module PseudoFunctorialityUnbiasedPadding (NKL : EHArgsS) = struct
+  module UP = UnbiasedPadding (NKL)
+
+  let x = Var.Db 0
+  let w = Var.Db 2
+  let ty = snd UP.v_constr
+  let ctx = (w, (ty, true)) :: UP.ctx
+  let w_constr = (Var w, ty)
+  let x_constr = (Var x, Obj)
+  let v_constr = UP.v_constr
+
+  let assoc n =
+    let tree = Builtin.Comp.tree 6 in
+    let f i = Builtin.Comp.f i in
+    let ty =
+      Construct.(
+        arr
+          (wcomp (comp3 (f 1) (f 2) (f 3)) 0 (comp3 (f 4) (f 5) (f 6)))
+          (comp3 (f 1) (comp3 (f 2) (wcomp (f 3) 0 (f 4)) (f 5)) (f 6)))
+    in
+    Suspension.coh (Some n) (check_coh tree ty ("_builtin_assoc", 0, []))
+
+  let unitor n =
+    let tree = Builtin.Comp.tree 2 in
+    let f i = Builtin.Comp.f i in
+    let x i = Builtin.Comp.x i in
+    let ty =
+      Construct.(arr (comp3 (f 1) (id_n 1 (x 1)) (f 2)) (wcomp (f 1) 0 (f 2)))
+    in
+    Suspension.coh (Some n) (check_coh tree ty ("_builtin_unitor", 0, []))
+
+  let intch n i =
+    assert (n >= 2);
+    let ps =
+      Br [ Br []; Suspension.ps (Some (n - 2)) (Br [ Br []; Br [] ]); Br [] ]
+    in
+    let tdb i = Var (Var.Db i) in
+    let d_L = (tdb 2, Arr (Obj, tdb 0, tdb 1)) in
+    let d_R = (tdb ((2 * n) + 6), Arr (Obj, tdb 3, tdb ((2 * n) + 5))) in
+    let d_max i =
+      let rec ty k =
+        if k = 1 then Arr (Obj, tdb 1, tdb 3)
+        else Arr (ty (k - 1), tdb (2 * k), tdb ((2 * k) + 1))
+      in
+      let d i =
+        let lvl = if i = 0 then 2 * n else (2 * n) + (2 * i) - 1 in
+        (tdb lvl, ty (n - 1))
+      in
+      (tdb ((2 * n) + (2 * i)), Construct.arr (d (i - 1)) (d i))
+    in
+    let ty =
+      Construct.(
+        arr
+          (comp
+             (wcomp_n 0 [ d_L; d_max 1; d_R ])
+             (wcomp_n 0 [ d_L; d_max 2; d_R ]))
+          (wcomp_n 0 [ d_L; comp_n [ d_max 1; d_max 2 ]; d_R ]))
+    in
+    Suspension.coh (Some i)
+      (check_coh ps ty ("_builtin_intch_chi" ^ string_of_int n, 0, []))
+
+  let rec psfpad_aux i =
+    let m = UP.F.min in
+    let n = UP.F.max in
+    let v_c = v_constr in
+    let w_c = w_constr in
+    let w_sub = [ w_constr; x_constr ] in
+    let witness_constr =
+      match i with
+      | i when i = m -> Construct.id_n 1 (Construct.wcomp v_c (n - 1) w_c)
+      | i when m < i -> (
+          let p, q = (UP.D.p (i - 1), UP.D.q (i - 1)) in
+          let p, q = (Tm.constr p, Tm.constr q) in
+          let t = UP.padded_func (i - 1) (n - i + 1) in
+          let tv = Tm.constr t in
+          let tw = Construct.tm_app t w_sub in
+          match i with
+          | i when i < n ->
+              let intch =
+                Construct.coh_app (intch (n - i + 1) (i - 1)) [ p; tv; tw; q ]
+              in
+              Construct.wcomp intch n
+                (Construct.wcomp_n (i - 1)
+                   [ p; Tm.constr (psfpad_aux (i - 1)); q ])
+          | i when i = n ->
+              let assoc =
+                Construct.coh_app (assoc (n - 1)) [ p; tv; q; p; tw; q ]
+              in
+              let w = Construct.witness q in
+              let unitor = Construct.coh_app (unitor (n - 1)) [ tv; tw ] in
+              Construct.comp_n
+                [
+                  assoc;
+                  Construct.wcomp_n (n - 1)
+                    [ p; Construct.wcomp_n (n - 1) [ tv; w; tw ]; q ];
+                  Construct.wcomp_n (n - 1) [ p; unitor; q ];
+                  Construct.wcomp_n (n - 1)
+                    [ p; Tm.constr (psfpad_aux (n - 1)); q ];
+                ]
+          | _ ->
+              Error.fatal
+                "[EH] Wrong arguments in pseudofunctoriality of padding")
+      | _ ->
+          Error.fatal "[EH] Wrong arguments in pseudofunctoriality of padding"
+    in
+    check_constr ctx witness_constr
+
+  let psfpad = psfpad_aux NKL.n
+end
+
+module EHCtx (NKL : EHArgsS) = struct
+  let x = Var.Db 0
+  let a = Var.Db 1
+  let b = Var.Db 2
+  let id = Construct.id_n (NKL.n - 1) (Var x, Obj)
+  let ty = Construct.arr id id
+  let ctx = [ (b, (ty, true)); (a, (ty, true)); (x, (Obj, false)) ]
+  let x_constr = (Var x, Obj)
+  let a_constr = (Var a, ty)
+  let b_constr = (Var b, ty)
+
+  let a_comp_id =
+    if NKL.l = NKL.n - 1 then a_constr
+    else Construct.wcomp a_constr NKL.l (Construct.id_n 1 id)
+
+  let id_comp_b =
+    if NKL.l = NKL.n - 1 then b_constr
+    else Construct.wcomp (Construct.id_n 1 id) NKL.l b_constr
+
+  module UP = UnbiasedPadding (NKL)
+
+  let a_comp_id_sub = [ a_comp_id; x_constr ]
+  let id_comp_b_sub = [ id_comp_b; x_constr ]
+end
+
+module BaseCases (NKL : EHArgsS) = struct
+  let intch n =
+    let ps = Br [ Unchecked.disc (n - 1); Unchecked.disc (n - 1) ] in
+    let rec disc_type_r = function
+      | 0 -> Obj
+      | 1 -> Arr (Obj, Var (Var.Db 1), Var (Var.Db ((2 * n) + 1)))
+      | k ->
+          Arr
+            ( disc_type_r (k - 1),
+              Var (Var.Db ((2 * n) + (2 * k) - 2)),
+              Var (Var.Db ((2 * n) + (2 * k) - 1)) )
+    in
+    let d_l = (Var (Var.Db (2 * n)), Unchecked.disc_type n) in
+    let d_r = (Var (Var.Db (4 * n)), disc_type_r n) in
+    let ty =
+      Construct.arr
+        (Construct.wcomp
+           (Construct.wcomp d_l 0 (Construct.id_n 1 (Construct.src 1 d_r)))
+           (n - 1)
+           (Construct.wcomp (Construct.id_n 1 (Construct.tgt 1 d_l)) 0 d_r))
+        (Construct.wcomp d_l 0 d_r)
+    in
+    let name = (Printf.sprintf "intch(%d,%d)" n 0, 0, []) in
+    check_coh ps ty name
+
+  module GT (N : BiasedPaddingArgsS) = struct
+    module BP = BackwardBiasedPadding (N)
+    module BToU = BackwardToUnbiasedRepadding (N)
+    module PSU = PseudoFunctorialityUnbiasedPadding (NKL)
+
+    let eh =
+      let open EHCtx (NKL) in
+      let step1 =
+        let p = BP.p in
+        let a_padded =
+          Construct.(
+            tm_app_sub p
+              (Unchecked.sub_ps_to_sub (characteristic_sub_ps a_constr)))
+        in
+        let b_padded =
+          Construct.(
+            tm_app_sub
+              (Opposite.checked_tm p [ 1 ])
+              (Unchecked.sub_ps_to_sub (characteristic_sub_ps b_constr)))
+        in
+        Construct.(develop (wcomp a_padded (NKL.n - 1) b_padded))
+      in
+      let step2 =
+        let r = BToU.repadded in
+        let r_op = Opposite.checked_tm r [ 1 ] in
+        let repad_a = Construct.tm_app r a_comp_id_sub in
+        let repad_b = Construct.tm_app r_op id_comp_b_sub in
+        Construct.wcomp repad_a (NKL.n - 1) repad_b
+      in
+      let step3 =
+        Construct.tm_app PSU.psfpad [ id_comp_b; a_comp_id; x_constr ]
+      in
+      let step4 =
+        let intch = Construct.coh_app (intch NKL.n) [ a_constr; b_constr ] in
+        Construct.tm_app
+          (Functorialisation.tm UP.padded [ (UP.v, 1) ])
+          [ intch; Construct.tgt 1 intch; Construct.src 1 intch; x_constr ]
+      in
+      Construct.comp_n [ step1; step2; step3; step4 ]
+  end
+
+  module LT (N : BiasedPaddingArgsS) = struct
+    module FP = ForwardBiasedPadding (N)
+    module FToU = ForwardToUnbiasedRepadding (N)
+    module PSU = PseudoFunctorialityUnbiasedPadding (NKL)
+
+    let eh =
+      let open EHCtx (NKL) in
+      let a_sub =
+        Unchecked.sub_ps_to_sub (Construct.characteristic_sub_ps a_constr)
+      in
+      let b_sub =
+        Unchecked.sub_ps_to_sub (Construct.characteristic_sub_ps b_constr)
+      in
+      let step1 =
+        Construct.inverse
+          (Construct.coh_app (intch NKL.n) [ a_constr; b_constr ])
+      in
+      let step2 =
+        let p = FP.p in
+        let a_padded = Construct.tm_app_sub p a_sub in
+        let b_padded =
+          Construct.(tm_app_sub (Opposite.checked_tm p [ 1 ]) b_sub)
+        in
+        Construct.(develop (wcomp a_padded (NKL.n - 1) b_padded))
+      in
+      let step3 =
+        let r = FToU.repadded in
+        let r_op = Opposite.checked_tm r [ 1 ] in
+        let repad_a = Construct.tm_app r [ a_constr; x_constr ] in
+        let repad_b = Construct.tm_app r_op [ b_constr; x_constr ] in
+        Construct.wcomp repad_a (NKL.n - 1) repad_b
+      in
+      let step4 =
+        Construct.tm_app PSU.psfpad [ b_constr; a_constr; x_constr ]
+      in
+      Construct.comp_n [ step1; step2; step3; step4 ]
+  end
+end
+
+let suspend eh_prev nkl =
+  let module NKL = (val nkl : EHArgsS) in
+  let open EHCtx (NKL) in
+  let module R = SuspUnbiasedToUnbiasedRepadding (NKL) in
+  let suspended_eh = Suspension.checked_tm (Some 1) eh_prev in
+  Construct.comp_n
+    [
+      Construct.tm_app suspended_eh
+        [ b_constr; a_constr; Construct.id x_constr; x_constr; x_constr ];
+      Construct.tm_app R.repadded
+        [ Construct.wcomp a_constr NKL.l b_constr; x_constr ];
+    ]
+
+module Naturality = struct
+  let nat_unitor constr =
+    let x_constr = (Var (Var.Db 0), Obj) in
+    let y_constr = (Var (Var.Db 1), Obj) in
+    let f_constr = (Var (Var.Db 2), Construct.arr x_constr y_constr) in
+    let cohty =
+      Construct.arr f_constr
+        (Construct.comp_n [ f_constr; Construct.id_n 1 y_constr ])
+    in
+    let runit = check_coh (Unchecked.disc 1) cohty ("_ehnat_step1", 0, []) in
+    let d = Construct.dim constr in
+    let sub = Construct.characteristic_sub_ps constr in
+    ( Coh (Suspension.coh (Some (d - 1)) runit, sub),
+      Unchecked.ty_apply_sub_ps (Suspension.ty (Some (d - 1)) cohty) sub )
+
+  let nat_factor eh_id_id nkl =
+    let module NKL = (val nkl : EHArgsS) in
+    let open EHCtx (NKL) in
+    let idn = Construct.id id in
+    let ty =
+      Construct.arr
+        (Construct.id (Construct.wcomp idn NKL.k idn))
+        (Construct.comp_n [ eh_id_id; Tm.constr UP.q ])
+    in
+
+    let name =
+      (Printf.sprintf "_factor_id(%d,%d,%d)" NKL.n NKL.k NKL.l, 0, [])
+    in
+    let coh = check_coh (Unchecked.disc 0) ty name in
+    Construct.of_coh coh
+
+  let nat_associator1 c1 c2 c3 =
+    let open Builtin.Comp in
+    let ty =
+      Construct.arr
+        (Construct.comp_n [ f 1; Construct.comp_n [ f 2; f 3 ] ])
+        (Construct.comp_n [ Construct.comp_n [ f 1; f 2 ]; f 3 ])
+    in
+    let coh = check_coh (tree 3) ty ("_assoc_left", 0, []) in
+    let d = Construct.dim c1 in
+    Construct.coh_app (Suspension.coh (Some (d - 1)) coh) [ c1; c2; c3 ]
+
+  let nat_associator2 c1 c2 c3 =
+    let open Builtin.Comp in
+    let ty =
+      Construct.arr
+        (Construct.comp_n [ Construct.comp_n [ f 1; f 2 ]; f 3 ])
+        (Construct.comp_n [ f 1; f 2; f 3 ])
+    in
+    let coh = check_coh (tree 3) ty ("_unbiasor_left", 0, []) in
+    let d = Construct.dim c1 in
+    Construct.coh_app (Suspension.coh (Some (d - 1)) coh) [ c1; c2; c3 ]
+
+  let nat_finalcoh eh_id_id nkl =
+    let module NKL = (val nkl : EHArgsS) in
+    let open EHCtx (NKL) in
+    let module UP = UnbiasedPadding (NKL) in
+    let p = Tm.constr UP.p in
+    let ty = Construct.arr eh_id_id p in
+    let name = (Printf.sprintf "_eh_to_p(%d,%d,%d)" NKL.n NKL.k NKL.l, 0, []) in
+    let coh = check_coh (Unchecked.disc 0) ty name in
+    Construct.of_coh coh
+
+  let compute eh_prev prev_nkl nkl =
+    let module PrevNKL = (val prev_nkl : EHArgsS) in
+    let open PrevNKL in
+    let module NKL = (val nkl : EHArgsS) in
+    let open EHCtx (NKL) in
+    let module Prev = EHCtx (PrevNKL) in
+    let module UP = UnbiasedPadding (PrevNKL) in
+    let q = Tm.constr UP.q in
+    let a_k_b = Construct.wcomp a_constr k b_constr in
+    let nat =
+      Construct.inverse
+        (Construct.tm_app
+           (Functorialisation.tm eh_prev [ (Prev.b, 1); (Prev.a, 1) ])
+           [ b_constr; id; id; a_constr; id; id; x_constr ])
+    in
+    let paddedfunc =
+      Construct.tm_app
+        (Functorialisation.tm UP.padded [ (UP.v, 1) ])
+        [
+          Construct.wcomp a_constr l b_constr;
+          UP.F.tgt_v (n + 1);
+          UP.F.src_v (n + 1);
+          x_constr;
+        ]
+    in
+    let eh_id_id = Construct.tm_app eh_prev [ id; id; x_constr ] in
+    Construct.comp_n
+      [
+        nat_unitor a_k_b;
+        Construct.wcomp a_k_b n (nat_factor eh_id_id prev_nkl);
+        nat_associator1 a_k_b eh_id_id q;
+        Construct.wcomp nat n q;
+        nat_associator2 eh_id_id paddedfunc q;
+        Construct.wcomp3 (nat_finalcoh eh_id_id prev_nkl) n paddedfunc n q;
+      ]
+end
+
+let rec eh nkl =
+  let module NKL = (val nkl : EHArgsS) in
+  let open NKL in
+  let module N = (val n_module n) in
+  let eh_constr =
+    if k = 0 && l = n - 1 then
+      let module BaseCases = BaseCases (NKL) in
+      let module BaseCase = BaseCases.LT (N) in
+      BaseCase.eh
+    else if k = n - 1 && l = 0 then
+      let module BaseCases = BaseCases (NKL) in
+      let module BaseCase = BaseCases.GT (N) in
+      BaseCase.eh
+    else if max k l = n - 1 then
+      let prevargs = nkl_module (n - 1) (k - 1) (l - 1) in
+      suspend (eh prevargs) nkl
+    else
+      let prevargs = nkl_module (n - 1) k l in
+      Naturality.compute (eh prevargs) prevargs nkl
+  in
+  let module C = EHCtx (NKL) in
+  check_constr C.ctx
+    ~name:(Printf.sprintf "eh^%d_(%d,%d)" n k l, 0, [])
+    eh_constr
+
+let full_eh nkl =
+  let eh = eh nkl in
+  let open (val nkl) in
+  let open EHCtx ((val nkl)) in
+  let constr =
+    Construct.comp_n
+      [
+        Construct.of_tm eh;
+        Construct.tm_app
+          (Inverse.inverse (Opposite.checked_tm eh [ l + 1 ]))
+          [ a_constr; b_constr; x_constr ];
+      ]
+  in
+  check_constr ctx constr
+
+let eh n k l = eh (nkl_module n k l)
+let full_eh n k l = full_eh (nkl_module n k l)
diff --git a/lib/eh.mli b/lib/eh.mli
new file mode 100644
index 00000000..44aab184
--- /dev/null
+++ b/lib/eh.mli
@@ -0,0 +1,4 @@
+open Kernel
+
+val eh : int -> int -> int -> Tm.t
+val full_eh : int -> int -> int -> Tm.t
diff --git a/lib/environment.ml b/lib/environment.ml
index 6a7d8665..c9501f78 100644
--- a/lib/environment.ml
+++ b/lib/environment.ml
@@ -12,6 +12,8 @@ let builtin_to_value b =
   | Conecomp (n, k, m) -> Tm (Cones.compose n m k)
   | Cylcomp (n, k, m) -> Tm (Cylinders.compose n m k)
   | Cylstack n -> Tm (Cylinders.stacking n)
+  | Eh_half (n, k, l) -> Tm (Eh.eh n k l)
+  | Eh_full (n, k, l) -> Tm (Eh.full_eh n k l)
 
 let value_ty v =
   match v with
diff --git a/lib/kernel.ml b/lib/kernel.ml
index 9f4a0639..5ce16da0 100644
--- a/lib/kernel.ml
+++ b/lib/kernel.ml
@@ -457,9 +457,6 @@ end = struct
   let ty t = Ty.forget t.ty
   let tbl : (Ctx.t * Types.tm, Tm.t) Hashtbl.t = Hashtbl.create 7829
 
-  (* TODO: this is incorrect: an applied term can be a variable *)
-  let to_var tm = match tm.e with Var v -> v | Coh _ | App _ -> raise IsCoh
-
   let free_vars tm =
     let fvty = Ty.free_vars tm.ty in
     match tm.e with
@@ -519,6 +516,16 @@ end = struct
         tm.developped <- Some dev;
         dev
 
+  let to_var tm =
+    match tm.e with
+    | Var v -> v
+    | Coh _ -> raise IsCoh
+    | App _ -> (
+        match develop tm with
+        | Var v -> v
+        | Coh _ -> raise IsCoh
+        | App _ | Meta_tm _ -> assert false)
+
   let apply_sub t sub =
     Ctx.check_equal (Sub.tgt sub) (Ty.ctx t.ty);
     let c = Sub.src sub in
diff --git a/lib/lexer.mll b/lib/lexer.mll
index 49717a32..5f358713 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -24,6 +24,16 @@ rule token = parse
   | "cylstack(" (['0'-'9']* as n) ")" {
                                       let n = int_of_string n in
                                       CYLSTACK(n) }
+  | "EH(" (['0'-'9']* as n) "," (['0'-'9']* as k) "," (['0'-'9']* as l)")" {
+                                                                            let n = int_of_string n in
+                                                                            let k = int_of_string k in
+                                                                            let l = int_of_string l in
+                                                                            EH_FULL(n,k,l) }
+  | "eh(" (['0'-'9']* as n) "," (['0'-'9']* as k) "," (['0'-'9']* as l)")" {
+                                                                            let n = int_of_string n in
+                                                                            let k = int_of_string k in
+                                                                            let l = int_of_string l in
+                                                                            EH_HALF(n,k,l) }                                                                        
   | "declare" { DECLARE }
   | "I" { INV }
   | "U" { UNIT }
diff --git a/lib/padding.ml b/lib/padding.ml
new file mode 100644
index 00000000..2e712f9d
--- /dev/null
+++ b/lib/padding.ml
@@ -0,0 +1,521 @@
+open Common
+open Kernel
+open Unchecked_types.Unchecked_types (Coh) (Tm)
+
+module type StringS = sig
+  val value : string
+end
+
+module Filtration = struct
+  (* Data defining a filtration *)
+  module type MakerS = sig
+    val min : int
+    val max : int
+    val ctx : int -> ctx
+    val v : int -> Var.t
+  end
+
+  (* Functions relative to a filtration *)
+  module type S = sig
+    include MakerS
+
+    val sub : int -> sub
+    val v_constr : int -> constr
+    val src_v : int -> constr
+    val tgt_v : int -> constr
+    val v_plus : int -> Var.t
+    val v_bridge : int -> Var.t
+    val in_plus : int -> sub
+    val in_minus : int -> sub
+  end
+
+  module Make (F : MakerS) : S = struct
+    include F
+
+    let v_constr i = (Var (F.v i), fst (List.assoc (F.v i) (F.ctx i)))
+    let src_v i = Construct.src 1 (v_constr i)
+    let tgt_v i = Construct.tgt 1 (v_constr i)
+
+    let to_db i =
+      let c = Functorialisation.ctx (F.ctx i) [ F.v i ] in
+      Unchecked.db_level_sub_inv c
+
+    let v_plus i = Display_maps.var_apply_sub (Var.Plus (F.v i)) (to_db i)
+    let v_bridge i = Display_maps.var_apply_sub (Var.Bridge (F.v i)) (to_db i)
+
+    let in_plus i =
+      let rec aux ctx =
+        match ctx with
+        | [] -> []
+        | (x, (_, _)) :: ctx when x == F.v i ->
+            (v i, (Var (v_plus i), false)) :: aux ctx
+        | (x, (_, b)) :: ctx ->
+            (x, (Unchecked.tm_apply_sub (Var x) (to_db i), b)) :: aux ctx
+      in
+      aux (F.ctx i)
+
+    let in_minus i =
+      let rec aux ctx =
+        match ctx with
+        | [] -> []
+        | (x, (_, _)) :: ctx when x == F.v i ->
+            (v i, (Var (v i), false)) :: aux ctx
+        | (x, (_, b)) :: ctx ->
+            (x, (Unchecked.tm_apply_sub (Var x) (to_db i), b)) :: aux ctx
+      in
+      aux (F.ctx i)
+
+    let sub i =
+      let w = v_constr (i + 1) in
+      let rec aux ctx =
+        match ctx with
+        | [] -> []
+        | (x, (_, _)) :: ctx when x = v i ->
+            (v_bridge i, (Construct.to_tm w, true))
+            :: (v_plus i, (Construct.(to_tm (tgt 1 w)), false))
+            :: (v i, (Construct.(to_tm (src 1 w)), false))
+            :: aux ctx
+        | (x, (_, b)) :: ctx -> (x, (Var x, b)) :: aux ctx
+      in
+      aux (ctx i)
+  end
+end
+
+module Padding = struct
+  let pad_one_step p q previous v sigma =
+    let prev =
+      Construct.tm_app_sub (Functorialisation.tm previous [ (v, 1) ]) sigma
+    in
+    Construct.comp3 (Tm.constr p) prev (Tm.constr q)
+
+  module type PaddingDataS = sig
+    val p : int -> Tm.t
+    val q : int -> Tm.t
+  end
+
+  module type PaddedS = sig
+    val padded : int -> Tm.t
+  end
+
+  module Padded (F : Filtration.S) (D : PaddingDataS) (Name : StringS) :
+    PaddedS = struct
+    let memo_padded : (int, Tm.t) Hashtbl.t = Hashtbl.create 77
+
+    let rec padded i =
+      let compute_padded i =
+        let name = (Printf.sprintf "%s.Padding(%d)" Name.value i, 0, []) in
+        let padded_constr =
+          if i = F.min then F.v_constr i
+          else
+            pad_one_step
+              (D.p (i - 1))
+              (D.q (i - 1))
+              (padded (i - 1))
+              (F.v (i - 1))
+              (F.sub (i - 1))
+        in
+        check_constr (F.ctx i) ~name padded_constr
+      in
+      match Hashtbl.find_opt memo_padded i with
+      | Some padded -> padded
+      | None ->
+          let padded = compute_padded i in
+          Hashtbl.add memo_padded i padded;
+          padded
+  end
+
+  (* Several padding data we consider are canonical -- they are given by a single
+     coherence in a well-chosen pasting scheme. The following aims at streamlining
+     the construction of such padding data *)
+  module type CanonicalPaddingDataArgsS = sig
+    val ps : int -> ps
+    val p_src : int -> constr
+    val q_tgt : int -> constr
+    val p_inc : int -> constr list
+    val q_inc : int -> constr list
+    val pad_in_ps : int -> sub
+  end
+
+  module CanonicalPaddingData
+      (F : Filtration.S)
+      (Args : CanonicalPaddingDataArgsS)
+      (P : PaddedS)
+      (Name : StringS) =
+  struct
+    let p i =
+      let padded_subbed =
+        Construct.tm_app_sub (P.padded i) (Args.pad_in_ps i)
+      in
+      let ty = Construct.arr (Args.p_src i) padded_subbed in
+      let name = (Printf.sprintf "%s.p(%d)" Name.value i, 0, []) in
+      let coh = check_coh (Args.ps i) ty name in
+      check_constr (F.ctx (i + 1)) (Construct.coh_app coh (Args.p_inc i))
+
+    let q i =
+      let padded_subbed =
+        Construct.tm_app_sub (P.padded i) (Args.pad_in_ps i)
+      in
+      let ty = Construct.arr padded_subbed (Args.q_tgt i) in
+      let name = (Printf.sprintf "%s.p(%d)" Name.value i, 0, []) in
+      let coh = check_coh (Args.ps i) ty name in
+      check_constr (F.ctx (i + 1)) (Construct.coh_app coh (Args.q_inc i))
+  end
+
+  module type MakerS = sig
+    module F : Filtration.S
+    module D : PaddingDataS
+    module P : PaddedS
+
+    val name : string
+  end
+
+  module type S = sig
+    include MakerS
+
+    val ctx : ctx
+    val v : Var.t
+    val v_constr : constr
+    val v_plus : Var.t
+    val v_bridge : Var.t
+    val p : Tm.t
+    val q : Tm.t
+    val padded : Tm.t
+    val padded_func : int -> int -> Tm.t
+  end
+
+  module Make (A : MakerS) : S = struct
+    module F = A.F
+
+    module D = struct
+      include A.D
+
+      let memo_p : (int, Tm.t) Hashtbl.t = Hashtbl.create 77
+      let memo_q : (int, Tm.t) Hashtbl.t = Hashtbl.create 77
+
+      let p i =
+        match Hashtbl.find_opt memo_p i with
+        | Some padded -> padded
+        | None ->
+            let padded = p i in
+            Hashtbl.add memo_p i padded;
+            padded
+
+      let q i =
+        match Hashtbl.find_opt memo_q i with
+        | Some padded -> padded
+        | None ->
+            let padded = q i in
+            Hashtbl.add memo_q i padded;
+            padded
+    end
+
+    module P = A.P
+
+    let name = A.name
+    let ctx = F.ctx F.max
+    let v = F.v F.max
+    let v_constr = F.v_constr F.max
+    let v_plus = F.v_plus F.max
+    let v_bridge = F.v_bridge F.max
+    let p = D.p F.max
+    let q = D.q F.max
+    let padded = P.padded F.max
+
+    (* Assumption: t is in the i-th context of the filtration *)
+    let rec iterated_func t i r =
+      match r with
+      | 0 -> t
+      | r ->
+          check_constr
+            (F.ctx (i + r))
+            (Construct.tm_app_sub
+               (Functorialisation.tm
+                  (iterated_func t i (r - 1))
+                  [ (F.v (i + r), 1) ])
+               (F.sub (i + r - 1)))
+
+    let padded_func i r = iterated_func (P.padded i) i r
+  end
+
+  module type MakerCanonicalS = sig
+    module F : Filtration.S
+    module D : CanonicalPaddingDataArgsS
+
+    val name : string
+  end
+
+  module MakeCanonical (A : MakerCanonicalS) = Make (struct
+    module F = A.F
+
+    let name = A.name
+
+    module Name : StringS = struct
+      let value = A.name
+    end
+
+    module rec D : PaddingDataS = CanonicalPaddingData (F) (A.D) (P) (Name)
+    and P : PaddedS = Padded (F) (D) (Name)
+  end)
+end
+
+module type FiltrationMorphismS = sig
+  val sub : int -> sub
+  val name : string
+end
+
+module PaddingApp
+    (Tgt : Filtration.S)
+    (M : FiltrationMorphismS)
+    (P : Padding.S) : Padding.S = Padding.Make (struct
+  module F = Tgt
+
+  module D = struct
+    let p i =
+      check_constr
+        (Tgt.ctx (i + 1))
+        (Construct.tm_app_sub (P.D.p i) (M.sub (i + 1)))
+
+    let q i =
+      check_constr
+        (Tgt.ctx (i + 1))
+        (Construct.tm_app_sub (P.D.q i) (M.sub (i + 1)))
+  end
+
+  let name = Printf.sprintf "%s[%s]" P.name M.name
+
+  module P = struct
+    let padded i =
+      check_constr (Tgt.ctx i) (Construct.tm_app_sub (P.P.padded i) (M.sub i))
+  end
+end)
+
+module Suspend (P : Padding.S) : Padding.S = Padding.Make (struct
+  module F = Filtration.Make (struct
+    let min = P.F.min + 1
+    let max = P.F.max + 1
+    let ctx i = Suspension.ctx (Some 1) (P.F.ctx (i - 1))
+    let v i = P.F.v i
+  end)
+
+  module D = struct
+    let p i = Suspension.checked_tm (Some 1) (P.D.p (i - 1))
+    let q i = Suspension.checked_tm (Some 1) (P.D.q (i - 1))
+  end
+
+  let name = Printf.sprintf "Σ%s" P.name
+
+  module P = struct
+    let padded i = Suspension.checked_tm (Some 1) (P.P.padded (i - 1))
+  end
+end)
+
+module Repadding = struct
+  let hexcomp fminus fplus ybridge fbridge gminus gplus gbridge zbridge hminus
+      hplus hbridge =
+    let d = Construct.dim fminus - 1 in
+    let db n = Var.Db n in
+    let hex =
+      Functorialisation.coh (Builtin.comp_n 3) [ db 6; db 4; db 3; db 2; db 1 ]
+    in
+    let hex = Suspension.checked_tm (Some d) hex in
+    let x = Construct.src 1 fminus in
+    let yminus = Construct.tgt 1 fminus in
+    let yplus = Construct.tgt 1 fplus in
+    let zminus = Construct.src 1 hminus in
+    let zplus = Construct.src 1 hplus in
+    let w = Construct.tgt 1 hminus in
+    let rec list_tgt_src ty =
+      match ty with
+      | Obj -> []
+      | Arr (a, u, v) -> (v, a) :: (u, a) :: list_tgt_src a
+      | _ -> assert false
+    in
+    let sub =
+      hbridge :: hplus :: hminus :: w :: gbridge :: gplus :: gminus :: zbridge
+      :: zplus :: zminus :: fbridge :: fplus :: fminus :: ybridge :: yplus
+      :: yminus :: x
+      :: list_tgt_src (snd w)
+    in
+    (* The call to sub_ps_to_sub is a bit of a hack, relying on the fact that all
+       checked terms use deBruijn. Further refactoring to be done in the kernel to
+       enforce this more statically *)
+    Construct.tm_app hex sub
+
+  let repad_one_step p_0 p_1 f q_0 q_1 g previous iota_minus iota_plus v sub =
+    let padding_0, padding_1 = Tm.bdry previous in
+    hexcomp (Tm.constr p_0) (Tm.constr p_1)
+      Construct.(apply_sub (tm_app_sub previous iota_minus) sub)
+      (Tm.constr f)
+      Construct.(tm_app_sub (Functorialisation.tm padding_0 [ (v, 1) ]) sub)
+      Construct.(tm_app_sub (Functorialisation.tm padding_1 [ (v, 1) ]) sub)
+      Construct.(
+        inverse (tm_app_sub (Functorialisation.tm previous [ (v, 1) ]) sub))
+      Construct.(apply_sub (tm_app_sub previous iota_plus) sub)
+      (Tm.constr q_0) (Tm.constr q_1) (Tm.constr g)
+
+  module type RepaddingDataS = sig
+    val f : int -> Tm.t
+    val g : int -> Tm.t
+  end
+
+  module type RepaddedS = sig
+    val repad : int -> Tm.t
+  end
+
+  module Repadded
+      (P1 : Padding.S)
+      (P2 : Padding.S)
+      (D : RepaddingDataS)
+      (Name : StringS) =
+  struct
+    let memo_repadded = Hashtbl.create 77
+
+    let rec repad i =
+      let compute_repadding i =
+        let repadding_constr =
+          if i = P1.F.min then Construct.id_n 1 (P1.F.v_constr i)
+          else
+            let previous = repad (i - 1) in
+            let sigma = P1.F.sub (i - 1) in
+            let f, g = (D.f (i - 1), D.g (i - 1)) in
+            repad_one_step
+              (P1.D.p (i - 1))
+              (P2.D.p (i - 1))
+              f
+              (P1.D.q (i - 1))
+              (P2.D.q (i - 1))
+              g previous
+              (P1.F.in_minus (i - 1))
+              (P1.F.in_plus (i - 1))
+              (P1.F.v (i - 1))
+              sigma
+        in
+        let name = (Printf.sprintf "%s.Repadding(%d)" Name.value i, 0, []) in
+        check_constr (P1.F.ctx i) ~name repadding_constr
+      in
+      match Hashtbl.find_opt memo_repadded i with
+      | Some t -> t
+      | None ->
+          let repadded = compute_repadding i in
+          Hashtbl.add memo_repadded i repadded;
+          repadded
+  end
+
+  module type CanonicalRepaddingDataArgsS = sig
+    val ps : int -> ps
+    val incl : int -> constr list
+  end
+
+  module CanonicalRepaddingData
+      (Args : CanonicalRepaddingDataArgsS)
+      (P1 : Padding.S)
+      (P2 : Padding.S)
+      (R : RepaddedS)
+      (Name : StringS) : RepaddingDataS = struct
+    let f i =
+      let ty =
+        Construct.(
+          arr
+            (wcomp
+               (Construct.develop (Tm.constr (P1.D.p i)))
+               i
+               (tm_app_sub (R.repad i)
+                  (Unchecked.sub_apply_sub (P1.F.in_minus i) (P1.F.sub i))))
+            (Construct.develop (Tm.constr (P2.D.p i))))
+      in
+      let name = (Printf.sprintf "%s.f(%d)" Name.value i, 0, []) in
+      let coh = check_coh (Args.ps i) ty name in
+      check_constr (P1.F.ctx i) (Construct.coh_app coh (Args.incl i))
+
+    let g i =
+      let ty =
+        Construct.(
+          arr
+            (Construct.develop (Tm.constr (P1.D.q i)))
+            (wcomp
+               (tm_app_sub (R.repad i)
+                  (Unchecked.sub_apply_sub (P1.F.in_plus i) (P1.F.sub i)))
+               i
+               (Construct.develop (Tm.constr (P2.D.q i)))))
+      in
+      let name = (Printf.sprintf "%s.g(%d)" Name.value i, 0, []) in
+      let coh = check_coh (Args.ps i) ty name in
+      check_constr (P1.F.ctx i) (Construct.coh_app coh (Args.incl i))
+  end
+
+  module type MakerS = sig
+    module P1 : Padding.S
+    module P2 : Padding.S
+    module D : RepaddingDataS
+    module R : RepaddedS
+
+    val name : string
+  end
+
+  module type S = sig
+    include MakerS
+
+    val repadded : Tm.t
+    val f : Tm.t
+    val g : Tm.t
+  end
+
+  module Make (A : MakerS) : S = struct
+    module P1 = A.P1
+    module P2 = A.P2
+
+    module D = struct
+      include A.D
+
+      let memo_f : (int, Tm.t) Hashtbl.t = Hashtbl.create 77
+      let memo_g : (int, Tm.t) Hashtbl.t = Hashtbl.create 77
+
+      let f i =
+        match Hashtbl.find_opt memo_f i with
+        | Some padded -> padded
+        | None ->
+            let padded = f i in
+            Hashtbl.add memo_f i padded;
+            padded
+
+      let g i =
+        match Hashtbl.find_opt memo_g i with
+        | Some padded -> padded
+        | None ->
+            let padded = g i in
+            Hashtbl.add memo_g i padded;
+            padded
+    end
+
+    module R = A.R
+
+    let name = A.name
+    let repadded = R.repad P1.F.max
+    let f = D.f (P1.F.max - 1)
+    let g = D.g (P1.F.max - 1)
+  end
+
+  module type MakerCanonicalS = sig
+    module P1 : Padding.S
+    module P2 : Padding.S
+    module D : CanonicalRepaddingDataArgsS
+
+    val name : string
+  end
+
+  module MakeCanonical (A : MakerCanonicalS) : S = Make (struct
+    module P1 = A.P1
+    module P2 = A.P2
+
+    module Name = struct
+      let value = A.name
+    end
+
+    let name = A.name
+
+    module rec D : RepaddingDataS =
+      CanonicalRepaddingData (A.D) (P1) (P2) (R) (Name)
+
+    and R : RepaddedS = Repadded (P1) (P2) (D) (Name)
+  end)
+end
diff --git a/lib/padding.mli b/lib/padding.mli
new file mode 100644
index 00000000..b0ec31e2
--- /dev/null
+++ b/lib/padding.mli
@@ -0,0 +1,141 @@
+open Common
+open Kernel
+open Unchecked_types.Unchecked_types(Coh)(Tm)
+
+module type StringS = sig
+  val value : string
+end
+
+module Filtration : sig
+  (* Data needed to define a filtration *)
+  module type MakerS = sig
+    val min : int
+    val max : int
+    val ctx : int -> ctx
+    val v : int -> Var.t
+  end
+
+  (* Data of the filtration *)
+  module type S = sig
+    include MakerS
+
+    val sub : int -> sub
+    val v_constr : int -> constr
+    val src_v : int -> constr
+    val tgt_v : int -> constr
+    val v_plus : int -> Var.t
+    val v_bridge : int -> Var.t
+    val in_plus : int -> sub
+    val in_minus : int -> sub
+  end
+
+  module Make (_ : MakerS) : S
+end
+
+module Padding : sig
+  module type PaddingDataS = sig
+    val p : int -> Tm.t
+    val q : int -> Tm.t
+  end
+
+  module type PaddedS = sig
+    val padded : int -> Tm.t
+  end
+
+  module type CanonicalPaddingDataArgsS = sig
+    val ps : int -> ps
+    val p_src : int -> constr
+    val q_tgt : int -> constr
+    val p_inc : int -> constr list
+    val q_inc : int -> constr list
+    val pad_in_ps : int -> sub
+  end
+
+  module type MakerS = sig
+    module F : Filtration.S
+    module D : PaddingDataS
+    module P : PaddedS
+
+    val name : string
+  end
+
+  module type S = sig
+    include MakerS
+
+    val ctx : ctx
+    val v : Var.t
+    val v_constr : constr
+    val v_plus : Var.t
+    val v_bridge : Var.t
+    val p : Tm.t
+    val q : Tm.t
+    val padded : Tm.t
+    val padded_func : int -> int -> Tm.t
+  end
+
+  module Make (_ : MakerS) : S
+
+  module type MakerCanonicalS = sig
+    module F : Filtration.S
+    module D : CanonicalPaddingDataArgsS
+
+    val name : string
+  end
+
+  module MakeCanonical (_ : MakerCanonicalS) : S
+end
+
+module type FiltrationMorphismS = sig
+  val sub : int -> sub
+  val name : string
+end
+
+module PaddingApp (_ : Filtration.S) (_ : FiltrationMorphismS) (_ : Padding.S) :
+  Padding.S
+
+module Suspend (_ : Padding.S) : Padding.S
+
+module Repadding : sig
+  module type RepaddingDataS = sig
+    val f : int -> Tm.t
+    val g : int -> Tm.t
+  end
+
+  module type RepaddedS = sig
+    val repad : int -> Tm.t
+  end
+
+  module type CanonicalRepaddingDataArgsS = sig
+    val ps : int -> ps
+    val incl : int -> constr list
+  end
+
+  module type MakerS = sig
+    module P1 : Padding.S
+    module P2 : Padding.S
+    module D : RepaddingDataS
+    module R : RepaddedS
+
+    val name : string
+  end
+
+  module type S = sig
+    include MakerS
+
+    val repadded : Tm.t
+    val f : Tm.t
+    val g : Tm.t
+  end
+
+  module Make (_ : MakerS) : S
+
+  module type MakerCanonicalS = sig
+    module P1 : Padding.S
+    module P2 : Padding.S
+    module D : CanonicalRepaddingDataArgsS
+
+    val name : string
+  end
+
+  module MakeCanonical (_ : MakerCanonicalS) : S
+end
diff --git a/lib/parser.mly b/lib/parser.mly
index 9cb03c6d..f49ac81a 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -37,6 +37,8 @@
 %token <string> BUILTIN
 %token <int*int*int> CONECOMP
 %token <int*int*int> CYLCOMP
+%token <int*int*int> EH_FULL
+%token <int*int*int> EH_HALF
 %token <int> CYLSTACK
 %token <string> IDENT
 %token <string> INT
@@ -114,6 +116,8 @@ builtin:
  | CONECOMP { let (n,k,m) = $1 in Conecomp(n,k,m) }
  | CYLCOMP { let (n,k,m) = $1 in Cylcomp(n,k,m) }
  | CYLSTACK { let n = $1 in Cylstack(n) }
+ | EH_HALF { let (n,k,l) = $1 in Eh_half(n,k,l)}
+ | EH_FULL { let (n,k,l) = $1 in Eh_full(n,k,l)}
 
 simple_tmexpr:
   | LPAR tmexpr RPAR { $2 }
diff --git a/lib/raw.ml b/lib/raw.ml
index f2dba944..b2dfa1dc 100644
--- a/lib/raw.ml
+++ b/lib/raw.ml
@@ -8,6 +8,8 @@ let string_of_builtin = function
   | Conecomp (n, k, m) -> Printf.sprintf "conecomp(%d,%d,%d)" n k m
   | Cylcomp (n, k, m) -> Printf.sprintf "cylcomp(%d,%d,%d)" n k m
   | Cylstack n -> Printf.sprintf "cylstack(%d)" n
+  | Eh_half (n , k , l) -> Printf.sprintf "eh^%d_(%d,%d)" n k l
+  | Eh_full (n , k , l) -> Printf.sprintf "EH^%d_(%d,%d)" n k l
 
 let rec string_of_ty e =
   match e with
@@ -124,6 +126,7 @@ and dim_builtin = function
   | Id -> 1
   | Conecomp (n, _, m) | Cylcomp (n, _, m) -> max n m
   | Cylstack n -> n
+  | Eh_half (n, _, _) | Eh_full (n, _, _) -> n + 1
 
 let rec dim_sub ctx = function
   | [] -> (0, 0)
@@ -145,7 +148,8 @@ let rec infer_susp_tm ctx = function
                 match b with
                 | Comp -> 1
                 | Id -> 0
-                | Conecomp (n, _, _) | Cylcomp (n, _, _) | Cylstack n -> n)
+                | Conecomp (n, _, _) | Cylcomp (n, _, _) | Cylstack n -> n
+                | Eh_half (n, _, _) | Eh_full (n, _, _) -> n)
             | _ -> assert false
           in
           let d, func = dim_sub ctx s in
diff --git a/lib/raw_types.mli b/lib/raw_types.mli
index a700082a..908d2d71 100644
--- a/lib/raw_types.mli
+++ b/lib/raw_types.mli
@@ -6,6 +6,8 @@ type builtin =
   | Conecomp of (int * int * int)
   | Cylcomp of (int * int * int)
   | Cylstack of int
+  | Eh_half of (int * int * int)
+  | Eh_full of (int * int * int)
 
 type tyR = Letin_ty of Var.t * tmR * tyR | ObjR | ArrR of tmR * tmR
 
diff --git a/lib/translate_raw.ml b/lib/translate_raw.ml
index 66b303f8..d1ce4f3f 100644
--- a/lib/translate_raw.ml
+++ b/lib/translate_raw.ml
@@ -60,6 +60,12 @@ let rec tm t =
           make_app tm s susp expl
       | Cylstack n ->
           let tm = Cylinders.stacking n in
+          make_app tm s susp expl
+      | Eh_half (n, k, l) ->
+          let tm = Eh.eh n k l in
+          make_app tm s susp expl
+      | Eh_full (n, k, l) ->
+          let tm = Eh.full_eh n k l in
           make_app tm s susp expl)
   | Op (l, t) ->
       let offset = head_susp t in
diff --git a/lib/unchecked.ml b/lib/unchecked.ml
index b55b8d97..0abea270 100644
--- a/lib/unchecked.ml
+++ b/lib/unchecked.ml
@@ -582,6 +582,15 @@ struct
             s
       | Meta_tm _ -> Error.fatal "meta-variables should be resolved"
 
+    let rec ty_contains_var a x =
+      match a with
+      | Obj -> false
+      | Arr (a, t, u) ->
+          tm_contains_var t x || tm_contains_var u x || ty_contains_var a x
+      | Meta_ty _ -> Error.fatal "meta-variables should be resolved"
+
+    let tm_contains_vars t l = List.exists (tm_contains_var t) l
+
     let rec check_equal_ps ps1 ps2 =
       match (ps1, ps2) with
       | Br [], Br [] -> ()
@@ -664,15 +673,6 @@ struct
     let check_equal_ctx ctx1 ctx2 =
       if ctx1 == ctx2 then () else check_equal_ctx ctx1 ctx2
 
-    let rec ty_contains_var a x =
-      match a with
-      | Obj -> false
-      | Arr (a, t, u) ->
-          tm_contains_var t x || tm_contains_var u x || ty_contains_var a x
-      | Meta_ty _ -> Error.fatal "meta-variables should be resolved"
-
-    let tm_contains_vars t l = List.exists (tm_contains_var t) l
-
     let rec list_to_sub s ctx =
       match (s, ctx) with
       | t :: s, (x, (_, expl)) :: ctx -> (x, (t, expl)) :: list_to_sub s ctx
diff --git a/test.t/features/eh.catt b/test.t/features/eh.catt
new file mode 100644
index 00000000..5b2f000a
--- /dev/null
+++ b/test.t/features/eh.catt
@@ -0,0 +1,15 @@
+check eh(2,0,1)
+check eh(3,0,1)
+check eh(4,2,1)
+check eh(3,1,2)
+check eh(4,3,2)
+check eh(3,1,2)
+check eh(4,2,3)
+check eh(3,0,2)
+check eh(2,1,0)
+check eh(3,2,0)
+check EH(2,0,1)
+check EH(3,0,1)
+check EH(3,1,2)
+check EH(3,1,2)
+check EH(3,2,0)
diff --git a/test.t/run.t b/test.t/run.t
index f7eb3036..f605911b 100644
--- a/test.t/run.t
+++ b/test.t/run.t
@@ -667,3 +667,107 @@
   [=I.I=] successfully defined term (!1builtin_comp3 [(Ilsimp x)] [(!2builtin_comp2 (!1builtin_comp3 (builtin_comp2 (builtin_id x) [a]) [(!2builtin_comp2 (!1builtin_comp2 [(lsimp x)] [(Ilsimp_op{1} x)]) (unit_Unit x))] (builtin_comp2 [b] (builtin_id x))) (exch b a))] [(lsimp_op{1} x)]) of type (!1builtin_comp3 (unitl^-1 (builtin_id x)) (!1builtin_comp3 (builtin_comp2 (builtin_id x) [a]) (!1builtin_comp2 (unitl (builtin_id x)) (unitl_op{1}^-1 (builtin_id x))) (builtin_comp2 [b] (builtin_id x))) (unitl_op{1} (builtin_id x))) -> (!1builtin_comp3 (unit^-1 x) (builtin_comp2 [b] [a]) (unit_op{1} x)).
   [=^.^=] let eh = (_builtin_comp  (eh1  a b) (eh2  a b) I(op_{1}((eh2  b a))) I(op_{1}((eh1  b a))))
   [=I.I=] successfully defined term (!2builtin_comp4 (eh1 a b) (eh2 a b) (!1builtin_comp3 [(Ilsimp_op{1}^-1 x)] [(!2builtin_comp2 (exch_op{1}^-1 b a) (!1builtin_comp3 (builtin_comp2_func[(.6,1)]_op{1} (builtin_id x) b) [(!2builtin_comp2 (unit_Unit_op{1}^-1 x) (!1builtin_comp2 [(lsimp_op{1}^-1 x)] [(Ilsimp_op{1}_op{1}^-1 x)]))] (builtin_comp2_func[(.4,1)]_op{1} a (builtin_id x))))] [(lsimp_op{1}_op{1}^-1 x)]) (eh1_op{1}^-1 b a)) of type (!1builtin_comp2 a b) -> (!1builtin_comp2_op{1} b a).
+
+  $ catt --no-builtins features/cones.catt
+  [=^.^=] check conecomp(2,1,2)
+  [=I.I=] valid term builtin_conecomp(2,1,2) of type .4 -> (builtin_comp2 (builtin_comp2 .2 .8) .9).
+  [=^.^=] check conecomp(3,1,3)
+  [=I.I=] valid term builtin_conecomp(3,1,3) of type (!1builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 .8 (builtin_comp2 .2 [.16])) (assoc .2 .12 .15)) (builtin_comp2 [(builtin_comp2 [.4] [.14])] .15)) -> (!1builtin_comp2 (!1builtin_comp2 .9 (builtin_comp2 .3 [.17])) (assoc .3 .13 .15)).
+  [=^.^=] check conecomp(3,2,3)
+  [=I.I=] valid term builtin_conecomp(3,2,3) of type (!1builtin_comp2 .8 (builtin_comp2 [(!1builtin_comp2 .4 .12)] .7)) -> .13.
+  [=^.^=] check conecomp(3,1,2)
+  [=I.I=] valid term builtin_conecomp(3,1,2) of type (!1builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 .8 (builtin_comp2 .2 [.14])) (assoc .2 .12 .13)) (builtin_comp2 [(builtin_comp2 [.4] .12)] .13)) -> (!1builtin_comp2 (!1builtin_comp2 .9 (builtin_comp2 .3 [.14])) (assoc .3 .12 .13)).
+  [=^.^=] check conecomp(2,1,3)
+  [=I.I=] valid term builtin_conecomp(2,1,3) of type (!1builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 .6 (builtin_comp2 .2 [.12])) (assoc .2 .8 .11)) (builtin_comp2 [(builtin_comp2 .2 [.10])] .11)) -> (!1builtin_comp2 (!1builtin_comp2 .6 (builtin_comp2 .2 [.13])) (assoc .2 .9 .11)).
+  [=^.^=] check conecomp(4,1,4)
+  [=I.I=] valid term builtin_conecomp(4,1,4) of type (!2builtin_comp3 (intch_src (!1builtin_comp2 .10 (builtin_comp2 .2 [.22])) (assoc .2 .16 .21) (builtin_comp2 [(builtin_comp2 [.4] [.18])] .21)) (!1builtin_comp2_red [(!2builtin_comp4 (!1builtin_assc (!1builtin_comp2 .10 (builtin_comp2 .2 [.22])) (assoc .2 .16 .21) (builtin_comp2 [(builtin_comp2 [.4] [.18])] .21)) (!1builtin_comp2 (!1builtin_comp2 .10 (builtin_comp2 .2 [.22])) [(assoc [.4] [.18] .21)]) (!1assoc (!1builtin_comp2 .10 (builtin_comp2 .2 [.22])) (builtin_comp2 [.4] [(builtin_comp2 [.18] .21)]) (assoc .3 .17 .21)) (!1builtin_comp2 [(@!1builtin_comp2 _ _ _ [_] [.12] [_] [(@builtin_comp2_func[(.6,1)] _ _ [.4] _ _ [_] [.24])])] (assoc .3 .17 .21)))]) (intch_tgt .8 (!1builtin_comp2 .11 (builtin_comp2 .3 [.23])) (assoc .3 .17 .21))) -> (!2builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 .10 (builtin_comp2 .2 [.22])) (assoc .2 .16 .21)) [(builtin_comp2 [[(builtin_comp2 [[.6]] [[.20]])]] .21)]) (!2builtin_comp3 (intch_src (!1builtin_comp2 .10 (builtin_comp2 .2 [.22])) (assoc .2 .16 .21) (builtin_comp2 [(builtin_comp2 [.5] [.19])] .21)) (!1builtin_comp2_red [(!2builtin_comp4 (!1builtin_assc (!1builtin_comp2 .10 (builtin_comp2 .2 [.22])) (assoc .2 .16 .21) (builtin_comp2 [(builtin_comp2 [.5] [.19])] .21)) (!1builtin_comp2 (!1builtin_comp2 .10 (builtin_comp2 .2 [.22])) [(assoc [.5] [.19] .21)]) (!1assoc (!1builtin_comp2 .10 (builtin_comp2 .2 [.22])) (builtin_comp2 [.5] [(builtin_comp2 [.19] .21)]) (assoc .3 .17 .21)) (!1builtin_comp2 [(@!1builtin_comp2 _ _ _ [_] [.13] [_] [(@builtin_comp2_func[(.6,1)] _ _ [.5] _ _ [_] [.25])])] (assoc .3 .17 .21)))]) (intch_tgt .8 (!1builtin_comp2 .11 (builtin_comp2 .3 [.23])) (assoc .3 .17 .21)))).
+  [=^.^=] check conecomp(4,2,4)
+  [=I.I=] valid term builtin_conecomp(4,2,4) of type (!2builtin_comp2 (!1builtin_comp2 .10 [(builtin_comp_1_0_intch .4 .16 .9)]) (!2builtin_comp2 (!1assoc .10 (builtin_comp2 [.4] .9) (builtin_comp2 [.16] .9)) (!1!1builtin_comp2_op{1,2} .20 (!1builtin_comp2_func[(.6,1)]_op{1,2} (builtin_comp2 [.16] .9) .12)))) -> (!2builtin_comp2 (!1builtin_comp2 .10 [(builtin_comp2 [[(!1builtin_comp2 [.6] [.18])]] .9)]) (!2builtin_comp2 (!1builtin_comp2 .10 [(builtin_comp_1_0_intch .5 .17 .9)]) (!2builtin_comp2 (!1assoc .10 (builtin_comp2 [.5] .9) (builtin_comp2 [.17] .9)) (!1!1builtin_comp2_op{1,2} .21 (!1builtin_comp2_func[(.6,1)]_op{1,2} (builtin_comp2 [.17] .9) .13))))).
+  [=^.^=] check conecomp(4,3,4)
+  [=I.I=] valid term builtin_conecomp(4,3,4) of type .12 -> (!2builtin_comp2 (!1builtin_comp2 .10 [(builtin_comp2 [[(!2builtin_comp2 .6 .16)]] .9)]) .17).
+  [=^.^=] check conecomp(4,1,2)
+  [=I.I=] valid term builtin_conecomp(4,1,2) of type (!2builtin_comp3 (intch_src (!1builtin_comp2 .10 (builtin_comp2 .2 [.18])) (assoc .2 .16 .17) (builtin_comp2 [(builtin_comp2 [.4] .16)] .17)) (!1builtin_comp2_red [(!2builtin_comp4 (!1builtin_assc (!1builtin_comp2 .10 (builtin_comp2 .2 [.18])) (assoc .2 .16 .17) (builtin_comp2 [(builtin_comp2 [.4] .16)] .17)) (!1builtin_comp2 (!1builtin_comp2 .10 (builtin_comp2 .2 [.18])) [(assoc [.4] .16 .17)]) (!1assoc (!1builtin_comp2 .10 (builtin_comp2 .2 [.18])) (builtin_comp2 [.4] (builtin_comp2 .16 .17)) (assoc .3 .16 .17)) (!1builtin_comp2 [(@!1builtin_comp2 _ _ _ [_] [.12] [_] [(builtin_comp2_func[(.8,1)] [.4] .18)])] (assoc .3 .16 .17)))]) (intch_tgt .8 (!1builtin_comp2 .11 (builtin_comp2 .3 [.18])) (assoc .3 .16 .17))) -> (!2builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 .10 (builtin_comp2 .2 [.18])) (assoc .2 .16 .17)) [(builtin_comp2 [[(builtin_comp2 [[.6]] .16)]] .17)]) (!2builtin_comp3 (intch_src (!1builtin_comp2 .10 (builtin_comp2 .2 [.18])) (assoc .2 .16 .17) (builtin_comp2 [(builtin_comp2 [.5] .16)] .17)) (!1builtin_comp2_red [(!2builtin_comp4 (!1builtin_assc (!1builtin_comp2 .10 (builtin_comp2 .2 [.18])) (assoc .2 .16 .17) (builtin_comp2 [(builtin_comp2 [.5] .16)] .17)) (!1builtin_comp2 (!1builtin_comp2 .10 (builtin_comp2 .2 [.18])) [(assoc [.5] .16 .17)]) (!1assoc (!1builtin_comp2 .10 (builtin_comp2 .2 [.18])) (builtin_comp2 [.5] (builtin_comp2 .16 .17)) (assoc .3 .16 .17)) (!1builtin_comp2 [(@!1builtin_comp2 _ _ _ [_] [.13] [_] [(builtin_comp2_func[(.8,1)] [.5] .18)])] (assoc .3 .16 .17)))]) (intch_tgt .8 (!1builtin_comp2 .11 (builtin_comp2 .3 [.18])) (assoc .3 .16 .17)))).
+  [=^.^=] check conecomp(4,1,3)
+  [=I.I=] valid term builtin_conecomp(4,1,3) of type (!2builtin_comp3 (intch_src (!1builtin_comp2 .10 (builtin_comp2 .2 [.20])) (assoc .2 .16 .19) (builtin_comp2 [(builtin_comp2 [.4] [.18])] .19)) (!1builtin_comp2_red [(!2builtin_comp4 (!1builtin_assc (!1builtin_comp2 .10 (builtin_comp2 .2 [.20])) (assoc .2 .16 .19) (builtin_comp2 [(builtin_comp2 [.4] [.18])] .19)) (!1builtin_comp2 (!1builtin_comp2 .10 (builtin_comp2 .2 [.20])) [(assoc [.4] [.18] .19)]) (!1assoc (!1builtin_comp2 .10 (builtin_comp2 .2 [.20])) (builtin_comp2 [.4] [(builtin_comp2 [.18] .19)]) (assoc .3 .17 .19)) (!1builtin_comp2 [(@!1builtin_comp2 _ _ _ [_] [.12] [_] [(@builtin_comp2_func[(.6,1)] _ _ [.4] _ _ [_] [.22])])] (assoc .3 .17 .19)))]) (intch_tgt .8 (!1builtin_comp2 .11 (builtin_comp2 .3 [.21])) (assoc .3 .17 .19))) -> (!2builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 .10 (builtin_comp2 .2 [.20])) (assoc .2 .16 .19)) [(builtin_comp2 [[(builtin_comp2 [[.6]] [.18])]] .19)]) (!2builtin_comp3 (intch_src (!1builtin_comp2 .10 (builtin_comp2 .2 [.20])) (assoc .2 .16 .19) (builtin_comp2 [(builtin_comp2 [.5] [.18])] .19)) (!1builtin_comp2_red [(!2builtin_comp4 (!1builtin_assc (!1builtin_comp2 .10 (builtin_comp2 .2 [.20])) (assoc .2 .16 .19) (builtin_comp2 [(builtin_comp2 [.5] [.18])] .19)) (!1builtin_comp2 (!1builtin_comp2 .10 (builtin_comp2 .2 [.20])) [(assoc [.5] [.18] .19)]) (!1assoc (!1builtin_comp2 .10 (builtin_comp2 .2 [.20])) (builtin_comp2 [.5] [(builtin_comp2 [.18] .19)]) (assoc .3 .17 .19)) (!1builtin_comp2 [(@!1builtin_comp2 _ _ _ [_] [.13] [_] [(@builtin_comp2_func[(.6,1)] _ _ [.5] _ _ [_] [.22])])] (assoc .3 .17 .19)))]) (intch_tgt .8 (!1builtin_comp2 .11 (builtin_comp2 .3 [.21])) (assoc .3 .17 .19)))).
+  [=^.^=] check conecomp(2,1,4)
+  [=I.I=] valid term builtin_conecomp(2,1,4) of type (!2builtin_comp3 (intch_src (!1builtin_comp2 .6 (builtin_comp2 .2 [.14])) (assoc .2 .8 .13) (builtin_comp2 [(builtin_comp2 .2 [.10])] .13)) (!1builtin_comp2_red [(!2builtin_comp4 (!1builtin_assc (!1builtin_comp2 .6 (builtin_comp2 .2 [.14])) (assoc .2 .8 .13) (builtin_comp2 [(builtin_comp2 .2 [.10])] .13)) (!1builtin_comp2 (!1builtin_comp2 .6 (builtin_comp2 .2 [.14])) [(assoc .2 [.10] .13)]) (!1assoc (!1builtin_comp2 .6 (builtin_comp2 .2 [.14])) (builtin_comp2 .2 [(builtin_comp2 [.10] .13)]) (assoc .2 .9 .13)) (!1builtin_comp2 [(@!1builtin_comp2 _ _ _ _ .6 [_] [(@builtin_comp2_func[(.6,1)] _ _ .2 _ _ [_] [.16])])] (assoc .2 .9 .13)))]) (intch_tgt .4 (!1builtin_comp2 .6 (builtin_comp2 .2 [.15])) (assoc .2 .9 .13))) -> (!2builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 .6 (builtin_comp2 .2 [.14])) (assoc .2 .8 .13)) [(builtin_comp2 [[(builtin_comp2 .2 [[.12]])]] .13)]) (!2builtin_comp3 (intch_src (!1builtin_comp2 .6 (builtin_comp2 .2 [.14])) (assoc .2 .8 .13) (builtin_comp2 [(builtin_comp2 .2 [.11])] .13)) (!1builtin_comp2_red [(!2builtin_comp4 (!1builtin_assc (!1builtin_comp2 .6 (builtin_comp2 .2 [.14])) (assoc .2 .8 .13) (builtin_comp2 [(builtin_comp2 .2 [.11])] .13)) (!1builtin_comp2 (!1builtin_comp2 .6 (builtin_comp2 .2 [.14])) [(assoc .2 [.11] .13)]) (!1assoc (!1builtin_comp2 .6 (builtin_comp2 .2 [.14])) (builtin_comp2 .2 [(builtin_comp2 [.11] .13)]) (assoc .2 .9 .13)) (!1builtin_comp2 [(@!1builtin_comp2 _ _ _ _ .6 [_] [(@builtin_comp2_func[(.6,1)] _ _ .2 _ _ [_] [.17])])] (assoc .2 .9 .13)))]) (intch_tgt .4 (!1builtin_comp2 .6 (builtin_comp2 .2 [.15])) (assoc .2 .9 .13)))).
+  [=^.^=] check conecomp(3,1,4)
+  [=I.I=] valid term builtin_conecomp(3,1,4) of type (!2builtin_comp3 (intch_src (!1builtin_comp2 .8 (builtin_comp2 .2 [.18])) (assoc .2 .12 .17) (builtin_comp2 [(builtin_comp2 [.4] [.14])] .17)) (!1builtin_comp2_red [(!2builtin_comp4 (!1builtin_assc (!1builtin_comp2 .8 (builtin_comp2 .2 [.18])) (assoc .2 .12 .17) (builtin_comp2 [(builtin_comp2 [.4] [.14])] .17)) (!1builtin_comp2 (!1builtin_comp2 .8 (builtin_comp2 .2 [.18])) [(assoc [.4] [.14] .17)]) (!1assoc (!1builtin_comp2 .8 (builtin_comp2 .2 [.18])) (builtin_comp2 [.4] [(builtin_comp2 [.14] .17)]) (assoc .3 .13 .17)) (!1builtin_comp2 [(@!1builtin_comp2 _ _ _ [_] [.10] [_] [(@builtin_comp2_func[(.6,1)] _ _ [.4] _ _ [_] [.20])])] (assoc .3 .13 .17)))]) (intch_tgt .6 (!1builtin_comp2 .9 (builtin_comp2 .3 [.19])) (assoc .3 .13 .17))) -> (!2builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 (!1builtin_comp2 .8 (builtin_comp2 .2 [.18])) (assoc .2 .12 .17)) [(builtin_comp2 [[(builtin_comp2 [.4] [[.16]])]] .17)]) (!2builtin_comp3 (intch_src (!1builtin_comp2 .8 (builtin_comp2 .2 [.18])) (assoc .2 .12 .17) (builtin_comp2 [(builtin_comp2 [.4] [.15])] .17)) (!1builtin_comp2_red [(!2builtin_comp4 (!1builtin_assc (!1builtin_comp2 .8 (builtin_comp2 .2 [.18])) (assoc .2 .12 .17) (builtin_comp2 [(builtin_comp2 [.4] [.15])] .17)) (!1builtin_comp2 (!1builtin_comp2 .8 (builtin_comp2 .2 [.18])) [(assoc [.4] [.15] .17)]) (!1assoc (!1builtin_comp2 .8 (builtin_comp2 .2 [.18])) (builtin_comp2 [.4] [(builtin_comp2 [.15] .17)]) (assoc .3 .13 .17)) (!1builtin_comp2 [(@!1builtin_comp2 _ _ _ [_] [.10] [_] [(@builtin_comp2_func[(.6,1)] _ _ [.4] _ _ [_] [.21])])] (assoc .3 .13 .17)))]) (intch_tgt .6 (!1builtin_comp2 .9 (builtin_comp2 .3 [.19])) (assoc .3 .13 .17)))).
+  [=^.^=] check conecomp(4,2,3)
+  [=I.I=] valid term builtin_conecomp(4,2,3) of type (!2builtin_comp2 (!1builtin_comp2 .10 [(builtin_comp_1_0_intch .4 .16 .9)]) (!2builtin_comp2 (!1assoc .10 (builtin_comp2 [.4] .9) (builtin_comp2 [.16] .9)) (!1!1builtin_comp2_op{1,2} .18 (!1builtin_comp2_func[(.6,1)]_op{1,2} (builtin_comp2 [.16] .9) .12)))) -> (!2builtin_comp2 (!1builtin_comp2 .10 [(builtin_comp2 [[(!1builtin_comp2 [.6] .16)]] .9)]) (!2builtin_comp2 (!1builtin_comp2 .10 [(builtin_comp_1_0_intch .5 .16 .9)]) (!2builtin_comp2 (!1assoc .10 (builtin_comp2 [.5] .9) (builtin_comp2 [.16] .9)) (!1!1builtin_comp2_op{1,2} .18 (!1builtin_comp2_func[(.6,1)]_op{1,2} (builtin_comp2 [.16] .9) .13))))).
+  [=^.^=] check conecomp(3,2,4)
+  [=I.I=] valid term builtin_conecomp(3,2,4) of type (!2builtin_comp2 (!1builtin_comp2 .8 [(builtin_comp_1_0_intch .4 .12 .7)]) (!2builtin_comp2 (!1assoc .8 (builtin_comp2 [.4] .7) (builtin_comp2 [.12] .7)) (!1!1builtin_comp2_op{1,2} .16 (!1builtin_comp2_func[(.6,1)]_op{1,2} (builtin_comp2 [.12] .7) .10)))) -> (!2builtin_comp2 (!1builtin_comp2 .8 [(builtin_comp2 [[(!1builtin_comp2 .4 [.14])]] .7)]) (!2builtin_comp2 (!1builtin_comp2 .8 [(builtin_comp_1_0_intch .4 .13 .7)]) (!2builtin_comp2 (!1assoc .8 (builtin_comp2 [.4] .7) (builtin_comp2 [.13] .7)) (!1!1builtin_comp2_op{1,2} .17 (!1builtin_comp2_func[(.6,1)]_op{1,2} (builtin_comp2 [.13] .7) .10))))).
+
+  $ catt --no-builtins features/cylinders.catt
+  [=^.^=] check cylcomp(2,1,2)
+  [=I.I=] valid term builtin_conecomp(2,1,2) of type (builtin_comp2 (builtin_comp2 .2 .10) .13) -> (builtin_comp2 .6 (builtin_comp2 .5 .12)).
+  [=^.^=] check cylcomp(3,1,3)
+  [=I.I=] valid term builtin_conecomp(2,1,2)_func[(.26,1) (.22,1) (.18,1) (.14,1) (.9,1) (.4,1)]_op{3} of type (!1builtin_comp2 (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .18)] .23) (!1builtin_comp3 (intch_src_op{3} .3 .17 .23) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .17 .23) (builtin_comp2_op{2} .3 [.25]) (assoc_op{3} .3 .11 .21) (builtin_comp2_op{2} [.13] .21) (builtin_assc_op{3} .10 .8 .21))) (intch_tgt_op{3} .10 .8 .21))) -> (!1builtin_comp2 (!1builtin_comp3 (intch_src_op{3} .2 .16 .23) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .23) (builtin_comp2_op{2} .2 [.24]) (assoc_op{3} .2 .11 .20) (builtin_comp2_op{2} [.12] .20) (builtin_assc_op{3} .10 .7 .20))) (intch_tgt_op{3} .10 .7 .20)) (builtin_comp2_op{2} .10 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .9 .22)])).
+  [=^.^=] check cylcomp(3,2,3)
+  [=D.D=] substitution: (.0, .0) (.1, .6) (.2, (builtin_comp2 .2 .11)) (.3, (builtin_comp2 .3 .11)) (.4, (builtin_comp2 [.4] .11)) (.5, (builtin_comp2 .10 .7)) (.6, (builtin_comp2 .10 .8)) (.7, (builtin_comp2 .10 [.9])) (.8, .12) (.9, .13) (.10, .14) (.11, (builtin_comp2 .15 .11)) (.12, (builtin_comp2 [.16] .11)) (.13, (builtin_comp2 .10 .17)) (.14, (builtin_comp2 .10 [.18])) (.15, .19) (.16, .20)
+  
+  [=I.I=] valid term builtin_conecomp(3,2,3) of type (!1builtin_comp2 (builtin_comp2 [(!1builtin_comp2 .4 .16)] .11) .19) -> (!1builtin_comp2 .12 (builtin_comp2_func[(.4,1)]_op{1} (!1builtin_comp2 .9 .18) .10)).
+  [=^.^=] check cylcomp(3,1,2)
+  [=I.I=] valid term builtin_conecomp(2,1,2)_func[(.14,1) (.9,1) (.4,1)]_op{3} of type (!1builtin_comp2 (builtin_comp2_op{2} [(builtin_comp2_op{2} [.4] .16)] .19) (!1builtin_comp3 (intch_src_op{3} .3 .16 .19) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .16 .19) (builtin_comp2_op{2} .3 [.20]) (assoc_op{3} .3 .11 .18) (builtin_comp2_op{2} [.13] .18) (builtin_assc_op{3} .10 .8 .18))) (intch_tgt_op{3} .10 .8 .18))) -> (!1builtin_comp2 (!1builtin_comp3 (intch_src_op{3} .2 .16 .19) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .19) (builtin_comp2_op{2} .2 [.20]) (assoc_op{3} .2 .11 .18) (builtin_comp2_op{2} [.12] .18) (builtin_assc_op{3} .10 .7 .18))) (intch_tgt_op{3} .10 .7 .18)) (builtin_comp2_op{2} .10 [(builtin_comp2_op{2} [.9] .18)])).
+  [=^.^=] check cylcomp(2,1,3)
+  [=I.I=] valid term builtin_conecomp(2,1,2)_func[(.20,1) (.16,1) (.12,1)]_op{3} of type (!1builtin_comp2 (builtin_comp2_op{2} [(builtin_comp2_op{2} .2 [.12])] .17) (!1builtin_comp3 (intch_src_op{3} .2 .11 .17) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .11 .17) (builtin_comp2_op{2} .2 [.19]) (assoc_op{3} .2 .7 .15) (builtin_comp2_op{2} [.8] .15) (builtin_assc_op{3} .6 .5 .15))) (intch_tgt_op{3} .6 .5 .15))) -> (!1builtin_comp2 (!1builtin_comp3 (intch_src_op{3} .2 .10 .17) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .10 .17) (builtin_comp2_op{2} .2 [.18]) (assoc_op{3} .2 .7 .14) (builtin_comp2_op{2} [.8] .14) (builtin_assc_op{3} .6 .5 .14))) (intch_tgt_op{3} .6 .5 .14)) (builtin_comp2_op{2} .6 [(builtin_comp2_op{2} .5 [.16])])).
+  [=^.^=] check cylcomp(4,1,4)
+  [=I.I=] valid term builtin_conecomp(2,1,2)_func[(.26,1) (.22,1) (.18,1) (.14,1) (.9,1) (.4,1)]_op{3}_func[(.38,1) (.32,1) (.26,1) (.20,1) (.13,1) (.6,1)]_op{4} of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} (builtin_comp2_func[(.4,1) (.8,1)]_op{3} [.6] [.26]) .33)] (!1builtin_comp3 (intch_src_op{3} .3 .23 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .33) (builtin_comp2_op{2} .3 [.35]) (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29))) (intch_tgt_op{3} .14 .10 .29))) (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .5 .25)] .33) (intch_src_op{3} .3 .23 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .33) (builtin_comp2_op{2} .3 [.35]) (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29))) (intch_tgt_op{3} .14 .10 .29)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .5 .25)] .33) (intch_src_op{3} .3 .23 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .33) (builtin_comp2_op{2} .3 [.35]) (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29))) (intch_tgt_op{3} .14 .10 .29)) (!1builtin_comp3 [(intch_src_func[(.4,1) (.8,1)]_op{3} .5 .25 .33)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .33) (builtin_comp2_op{2} .3 [.35]) (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29))) (intch_tgt_op{3} .14 .10 .29)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .5 .25)] .33)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .33) (builtin_comp2_op{2} .3 [.35]) (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29))) (intch_tgt_op{3} .14 .10 .29)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .33) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.4,1) (.8,1)]_op{3} .5 .25 .33) (builtin_comp2_func[(.6,1)][(.2~,1) (.4~,1) (.5~,1) (.6~,1)]_op{3} .5 .37) (assoc_func[(.4,1) (.10,1)]_op{3} .5 .15 .31) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1) (.6~,1)]_op{3} .19 .31) (builtin_assc_func[(.6,1) (.10,1)]_op{3} .14 .12 .31)))] (intch_tgt_op{3} .14 .10 .29)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .33) (builtin_comp2_op{2} .2 [.34]) (assoc_op{3} .2 .15 .28) (builtin_comp2_op{2} [.16] .28) (builtin_assc_op{3} .14 .9 .28))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .12 .31)])) (intch_tgt_op{3} .14 .10 .29)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .33) (builtin_comp2_op{2} .2 [.34]) (assoc_op{3} .2 .15 .28) (builtin_comp2_op{2} [.16] .28) (builtin_assc_op{3} .14 .9 .28))) [(intch_tgt_func[(.6,1) (.10,1)]_op{3} .14 .12 .31)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .33) (builtin_comp2_op{2} .2 [.34]) (assoc_op{3} .2 .15 .28) (builtin_comp2_op{2} [.16] .28) (builtin_assc_op{3} .14 .9 .28))) (intch_tgt_op{3} .14 .9 .28) (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .12 .31)])))) (intch_src_op{3} (intch_src_op{3} .2 .22 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .33) (builtin_comp2_op{2} .2 [.34]) (assoc_op{3} .2 .15 .28) (builtin_comp2_op{2} [.16] .28) (builtin_assc_op{3} .14 .9 .28))) (intch_tgt_op{3} .14 .9 .28) (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .12 .31)])))) -> (!2builtin_comp2 (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .24)] .33) (intch_src_op{3} .3 .23 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .33) (builtin_comp2_op{2} .3 [.35]) (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29))) (intch_tgt_op{3} .14 .10 .29)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .24)] .33) (intch_src_op{3} .3 .23 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .33) (builtin_comp2_op{2} .3 [.35]) (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29))) (intch_tgt_op{3} .14 .10 .29)) (!1builtin_comp3 [(intch_src_func[(.4,1) (.8,1)]_op{3} .4 .24 .33)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .33) (builtin_comp2_op{2} .3 [.35]) (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29))) (intch_tgt_op{3} .14 .10 .29)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .24)] .33)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .33) (builtin_comp2_op{2} .3 [.35]) (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29))) (intch_tgt_op{3} .14 .10 .29)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .33) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.4,1) (.8,1)]_op{3} .4 .24 .33) (builtin_comp2_func[(.6,1)][(.2~,1) (.4~,1) (.5~,1) (.6~,1)]_op{3} .4 .36) (assoc_func[(.4,1) (.10,1)]_op{3} .4 .15 .30) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1) (.6~,1)]_op{3} .18 .30) (builtin_assc_func[(.6,1) (.10,1)]_op{3} .14 .11 .30)))] (intch_tgt_op{3} .14 .10 .29)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .33) (builtin_comp2_op{2} .2 [.34]) (assoc_op{3} .2 .15 .28) (builtin_comp2_op{2} [.16] .28) (builtin_assc_op{3} .14 .9 .28))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .11 .30)])) (intch_tgt_op{3} .14 .10 .29)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .33) (builtin_comp2_op{2} .2 [.34]) (assoc_op{3} .2 .15 .28) (builtin_comp2_op{2} [.16] .28) (builtin_assc_op{3} .14 .9 .28))) [(intch_tgt_func[(.6,1) (.10,1)]_op{3} .14 .11 .30)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .33) (builtin_comp2_op{2} .2 [.34]) (assoc_op{3} .2 .15 .28) (builtin_comp2_op{2} [.16] .28) (builtin_assc_op{3} .14 .9 .28))) (intch_tgt_op{3} .14 .9 .28) (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .11 .30)])))) (intch_src_op{3} (intch_src_op{3} .2 .22 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .33) (builtin_comp2_op{2} .2 [.34]) (assoc_op{3} .2 .15 .28) (builtin_comp2_op{2} [.16] .28) (builtin_assc_op{3} .14 .9 .28))) (intch_tgt_op{3} .14 .9 .28) (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .11 .30)]))) (!1builtin_comp2 (!1builtin_comp3 (intch_src_op{3} .2 .22 .33) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .33) (builtin_comp2_op{2} .2 [.34]) (assoc_op{3} .2 .15 .28) (builtin_comp2_op{2} [.16] .28) (builtin_assc_op{3} .14 .9 .28))) (intch_tgt_op{3} .14 .9 .28)) [(builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .14 (builtin_comp2_func[(.4,1) (.8,1)]_op{3} [.13] [.32]))])).
+  [=^.^=] check cylcomp(4,2,4)
+  [=I.I=] valid term builtin_conecomp(3,2,3)_func[(.32,1) (.28,1) (.24,1) (.20,1) (.13,1) (.6,1)]_op{4} of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} (!1builtin_comp2 [.6] [.24]) .15)] .29) (!2builtin_comp3 (!1builtin_comp2 [(builtin_comp_1_0_intch_op{4} .5 .23 .15)] .29) (!2builtin_comp3 (!1intch_src (builtin_comp2_op{2} [.5] .15) (builtin_comp2_op{2} [.23] .15) .29) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp5 (!1builtin_assc (builtin_comp2_op{2} [.5] .15) (builtin_comp2_op{2} [.23] .15) .29) (!1builtin_comp2 (builtin_comp2_op{2} [.5] .15) [.31]) (!1assoc (builtin_comp2_op{2} [.5] .15) .17 (builtin_comp2_op{2} .14 [.27])) (!1builtin_comp2 [.19] (builtin_comp2_op{2} .14 [.27])) (!1builtin_assc .16 (builtin_comp2_op{2} .14 [.12]) (builtin_comp2_op{2} .14 [.27])))) (!1intch_tgt .16 (builtin_comp2_op{2} .14 [.12]) (builtin_comp2_op{2} .14 [.27]))) (!1builtin_comp2 .16 [(builtin_comp_1_0_intch_op{1}^-1 .14 .12 .27)]))) -> (!2builtin_comp2 (!2builtin_comp3 (!1builtin_comp2 [(builtin_comp_1_0_intch_op{4} .4 .22 .15)] .29) (!2builtin_comp3 (!1intch_src (builtin_comp2_op{2} [.4] .15) (builtin_comp2_op{2} [.22] .15) .29) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp5 (!1builtin_assc (builtin_comp2_op{2} [.4] .15) (builtin_comp2_op{2} [.22] .15) .29) (!1builtin_comp2 (builtin_comp2_op{2} [.4] .15) [.30]) (!1assoc (builtin_comp2_op{2} [.4] .15) .17 (builtin_comp2_op{2} .14 [.26])) (!1builtin_comp2 [.18] (builtin_comp2_op{2} .14 [.26])) (!1builtin_assc .16 (builtin_comp2_op{2} .14 [.11]) (builtin_comp2_op{2} .14 [.26])))) (!1intch_tgt .16 (builtin_comp2_op{2} .14 [.11]) (builtin_comp2_op{2} .14 [.26]))) (!1builtin_comp2 .16 [(builtin_comp_1_0_intch_op{1}^-1 .14 .11 .26)])) (!1builtin_comp2 .16 [(builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .14 (!1builtin_comp2 [.13] [.28]))])).
+  [=^.^=] check cylcomp(4,3,4)
+  [=D.D=] substitution: (.0, .0) (.1, .6) (.2, (builtin_comp2 .2 .11)) (.3, (builtin_comp2 .3 .11)) (.4, (builtin_comp2 [.4] .11)) (.5, (builtin_comp2 .10 .7)) (.6, (builtin_comp2 .10 .8)) (.7, (builtin_comp2 .10 [.9])) (.8, .12) (.9, .13) (.10, .14) (.11, (builtin_comp2 .15 .11)) (.12, (builtin_comp2 [.16] .11)) (.13, (builtin_comp2 .10 .17)) (.14, (builtin_comp2 .10 [.18])) (.15, .19) (.16, .20)
+  
+  [=D.D=] substitution: (.0, .0) (.1, .8) (.2, (builtin_comp2 .2 .15)) (.3, (builtin_comp2 .3 .15)) (.4, (builtin_comp2 [.4] .15)) (.5, (builtin_comp2 [.5] .15)) (.6, (builtin_comp2 [[.6]] .15)) (.7, (builtin_comp2 .14 .9)) (.8, (builtin_comp2 .14 .10)) (.9, (builtin_comp2 .14 [.11])) (.10, (builtin_comp2 .14 [.12])) (.11, (builtin_comp2 .14 [[.13]])) (.12, .16) (.13, .17) (.14, .18) (.15, .19) (.16, .20) (.17, (builtin_comp2 [.21] .15)) (.18, (builtin_comp2 [[.22]] .15)) (.19, (builtin_comp2 .14 [.23])) (.20, (builtin_comp2 .14 [[.24]])) (.21, .25) (.22, .26)
+  
+  [=I.I=] valid term builtin_conecomp(4,3,4) of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2 [[(!2builtin_comp2 .6 .22)]] .15)] .17) .25) -> (!2builtin_comp2 .18 (!1builtin_comp2 .16 [(builtin_comp2_func[(.6,2)]_op{1} (!2builtin_comp2 .13 .24) .14)])).
+  [=^.^=] check cylcomp(4,1,2)
+  [=I.I=] valid term builtin_conecomp(2,1,2)_func[(.14,1) (.9,1) (.4,1)]_op{3}_func[(.20,1) (.13,1) (.6,1)]_op{4} of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} (builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} .6 .22) .25)] (!1builtin_comp3 (intch_src_op{3} .3 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24))) (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.5] .22)] .25) (intch_src_op{3} .3 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.5] .22)] .25) (intch_src_op{3} .3 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 [(intch_src_func[(.4,1)]_op{3} .5 .22 .25)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.5] .22)] .25)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .25) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.4,1)]_op{3} .5 .22 .25) (builtin_comp2_func[(.8,1)][(.4,1)]_op{3} .5 .26) (assoc_func[(.4,1)]_op{3} .5 .15 .24) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} .19 .24) (builtin_assc_func[(.6,1)]_op{3} .14 .12 .24)))] (intch_tgt_op{3} .14 .10 .24)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.12] .24)])) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) [(intch_tgt_func[(.6,1)]_op{3} .14 .12 .24)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (intch_tgt_op{3} .14 .9 .24) (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.12] .24)])))) (intch_src_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (intch_tgt_op{3} .14 .9 .24) (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.12] .24)])))) -> (!2builtin_comp2 (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.4] .22)] .25) (intch_src_op{3} .3 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.4] .22)] .25) (intch_src_op{3} .3 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 [(intch_src_func[(.4,1)]_op{3} .4 .22 .25)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.4] .22)] .25)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .25) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.4,1)]_op{3} .4 .22 .25) (builtin_comp2_func[(.8,1)][(.4,1)]_op{3} .4 .26) (assoc_func[(.4,1)]_op{3} .4 .15 .24) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} .18 .24) (builtin_assc_func[(.6,1)]_op{3} .14 .11 .24)))] (intch_tgt_op{3} .14 .10 .24)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.11] .24)])) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) [(intch_tgt_func[(.6,1)]_op{3} .14 .11 .24)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (intch_tgt_op{3} .14 .9 .24) (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.11] .24)])))) (intch_src_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (intch_tgt_op{3} .14 .9 .24) (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.11] .24)]))) (!1builtin_comp2 (!1builtin_comp3 (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (intch_tgt_op{3} .14 .9 .24)) [(builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .14 (builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} .13 .24))])).
+  [=^.^=] check cylcomp(4,1,3)
+  [=I.I=] valid term builtin_conecomp(2,1,2)_func[(.26,1) (.22,1) (.18,1) (.14,1) (.9,1) (.4,1)]_op{3}_func[(.20,1) (.13,1) (.6,1)]_op{4} of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} (builtin_comp2_func[(.6,1)]_red_func[(.6,1)]_op{3} .6 .24) .29)] (!1builtin_comp3 (intch_src_op{3} .3 .23 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .29) (builtin_comp2_op{2} .3 [.31]) (assoc_op{3} .3 .15 .27) (builtin_comp2_op{2} [.17] .27) (builtin_assc_op{3} .14 .10 .27))) (intch_tgt_op{3} .14 .10 .27))) (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .5 .24)] .29) (intch_src_op{3} .3 .23 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .29) (builtin_comp2_op{2} .3 [.31]) (assoc_op{3} .3 .15 .27) (builtin_comp2_op{2} [.17] .27) (builtin_assc_op{3} .14 .10 .27))) (intch_tgt_op{3} .14 .10 .27)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .5 .24)] .29) (intch_src_op{3} .3 .23 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .29) (builtin_comp2_op{2} .3 [.31]) (assoc_op{3} .3 .15 .27) (builtin_comp2_op{2} [.17] .27) (builtin_assc_op{3} .14 .10 .27))) (intch_tgt_op{3} .14 .10 .27)) (!1builtin_comp3 [(intch_src_func[(.4,1) (.8,1)]_op{3} .5 .24 .29)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .29) (builtin_comp2_op{2} .3 [.31]) (assoc_op{3} .3 .15 .27) (builtin_comp2_op{2} [.17] .27) (builtin_assc_op{3} .14 .10 .27))) (intch_tgt_op{3} .14 .10 .27)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .5 .24)] .29)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .29) (builtin_comp2_op{2} .3 [.31]) (assoc_op{3} .3 .15 .27) (builtin_comp2_op{2} [.17] .27) (builtin_assc_op{3} .14 .10 .27))) (intch_tgt_op{3} .14 .10 .27)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .29) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.4,1) (.8,1)]_op{3} .5 .24 .29) (builtin_comp2_func[(.6,1)][(.2~,1) (.4~,1) (.5~,1) (.6~,1)]_op{3} .5 .32) (assoc_func[(.4,1) (.10,1)]_op{3} .5 .15 .28) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1) (.6~,1)]_op{3} .19 .28) (builtin_assc_func[(.6,1) (.10,1)]_op{3} .14 .12 .28)))] (intch_tgt_op{3} .14 .10 .27)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .29) (builtin_comp2_op{2} .2 [.30]) (assoc_op{3} .2 .15 .26) (builtin_comp2_op{2} [.16] .26) (builtin_assc_op{3} .14 .9 .26))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .12 .28)])) (intch_tgt_op{3} .14 .10 .27)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .29) (builtin_comp2_op{2} .2 [.30]) (assoc_op{3} .2 .15 .26) (builtin_comp2_op{2} [.16] .26) (builtin_assc_op{3} .14 .9 .26))) [(intch_tgt_func[(.6,1) (.10,1)]_op{3} .14 .12 .28)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .29) (builtin_comp2_op{2} .2 [.30]) (assoc_op{3} .2 .15 .26) (builtin_comp2_op{2} [.16] .26) (builtin_assc_op{3} .14 .9 .26))) (intch_tgt_op{3} .14 .9 .26) (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .12 .28)])))) (intch_src_op{3} (intch_src_op{3} .2 .22 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .29) (builtin_comp2_op{2} .2 [.30]) (assoc_op{3} .2 .15 .26) (builtin_comp2_op{2} [.16] .26) (builtin_assc_op{3} .14 .9 .26))) (intch_tgt_op{3} .14 .9 .26) (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .12 .28)])))) -> (!2builtin_comp2 (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .24)] .29) (intch_src_op{3} .3 .23 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .29) (builtin_comp2_op{2} .3 [.31]) (assoc_op{3} .3 .15 .27) (builtin_comp2_op{2} [.17] .27) (builtin_assc_op{3} .14 .10 .27))) (intch_tgt_op{3} .14 .10 .27)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .24)] .29) (intch_src_op{3} .3 .23 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .29) (builtin_comp2_op{2} .3 [.31]) (assoc_op{3} .3 .15 .27) (builtin_comp2_op{2} [.17] .27) (builtin_assc_op{3} .14 .10 .27))) (intch_tgt_op{3} .14 .10 .27)) (!1builtin_comp3 [(intch_src_func[(.4,1) (.8,1)]_op{3} .4 .24 .29)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .29) (builtin_comp2_op{2} .3 [.31]) (assoc_op{3} .3 .15 .27) (builtin_comp2_op{2} [.17] .27) (builtin_assc_op{3} .14 .10 .27))) (intch_tgt_op{3} .14 .10 .27)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .24)] .29)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .23 .29) (builtin_comp2_op{2} .3 [.31]) (assoc_op{3} .3 .15 .27) (builtin_comp2_op{2} [.17] .27) (builtin_assc_op{3} .14 .10 .27))) (intch_tgt_op{3} .14 .10 .27)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .29) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.4,1) (.8,1)]_op{3} .4 .24 .29) (builtin_comp2_func[(.6,1)][(.2~,1) (.4~,1) (.5~,1) (.6~,1)]_op{3} .4 .32) (assoc_func[(.4,1) (.10,1)]_op{3} .4 .15 .28) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1) (.6~,1)]_op{3} .18 .28) (builtin_assc_func[(.6,1) (.10,1)]_op{3} .14 .11 .28)))] (intch_tgt_op{3} .14 .10 .27)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .29) (builtin_comp2_op{2} .2 [.30]) (assoc_op{3} .2 .15 .26) (builtin_comp2_op{2} [.16] .26) (builtin_assc_op{3} .14 .9 .26))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .11 .28)])) (intch_tgt_op{3} .14 .10 .27)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .29) (builtin_comp2_op{2} .2 [.30]) (assoc_op{3} .2 .15 .26) (builtin_comp2_op{2} [.16] .26) (builtin_assc_op{3} .14 .9 .26))) [(intch_tgt_func[(.6,1) (.10,1)]_op{3} .14 .11 .28)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .29) (builtin_comp2_op{2} .2 [.30]) (assoc_op{3} .2 .15 .26) (builtin_comp2_op{2} [.16] .26) (builtin_assc_op{3} .14 .9 .26))) (intch_tgt_op{3} .14 .9 .26) (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .11 .28)])))) (intch_src_op{3} (intch_src_op{3} .2 .22 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .29) (builtin_comp2_op{2} .2 [.30]) (assoc_op{3} .2 .15 .26) (builtin_comp2_op{2} [.16] .26) (builtin_assc_op{3} .14 .9 .26))) (intch_tgt_op{3} .14 .9 .26) (builtin_comp2_op{2} .14 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .11 .28)]))) (!1builtin_comp2 (!1builtin_comp3 (intch_src_op{3} .2 .22 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .29) (builtin_comp2_op{2} .2 [.30]) (assoc_op{3} .2 .15 .26) (builtin_comp2_op{2} [.16] .26) (builtin_assc_op{3} .14 .9 .26))) (intch_tgt_op{3} .14 .9 .26)) [(builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .14 (builtin_comp2_func[(.6,1)]_red_func[(.6,1)]_op{3} .13 .28))])).
+  [=^.^=] check cylcomp(2,1,4)
+  [=I.I=] valid term builtin_conecomp(2,1,2)_func[(.20,1) (.16,1) (.12,1)]_op{3}_func[(.26,1) (.20,1) (.14,1)]_op{4} of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} (builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .2 .14) .21)] (!1builtin_comp3 (intch_src_op{3} .2 .11 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .11 .21) (builtin_comp2_op{2} .2 [.23]) (assoc_op{3} .2 .7 .17) (builtin_comp2_op{2} [.8] .17) (builtin_assc_op{3} .6 .5 .17))) (intch_tgt_op{3} .6 .5 .17))) (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} .2 [.13])] .21) (intch_src_op{3} .2 .11 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .11 .21) (builtin_comp2_op{2} .2 [.23]) (assoc_op{3} .2 .7 .17) (builtin_comp2_op{2} [.8] .17) (builtin_assc_op{3} .6 .5 .17))) (intch_tgt_op{3} .6 .5 .17)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} .2 [.13])] .21) (intch_src_op{3} .2 .11 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .11 .21) (builtin_comp2_op{2} .2 [.23]) (assoc_op{3} .2 .7 .17) (builtin_comp2_op{2} [.8] .17) (builtin_assc_op{3} .6 .5 .17))) (intch_tgt_op{3} .6 .5 .17)) (!1builtin_comp3 [(intch_src_func[(.6,1)]_op{3} .2 .13 .21)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .11 .21) (builtin_comp2_op{2} .2 [.23]) (assoc_op{3} .2 .7 .17) (builtin_comp2_op{2} [.8] .17) (builtin_assc_op{3} .6 .5 .17))) (intch_tgt_op{3} .6 .5 .17)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .10 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} .2 [.13])] .21)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .11 .21) (builtin_comp2_op{2} .2 [.23]) (assoc_op{3} .2 .7 .17) (builtin_comp2_op{2} [.8] .17) (builtin_assc_op{3} .6 .5 .17))) (intch_tgt_op{3} .6 .5 .17)) (!1builtin_comp3 (intch_src_op{3} .2 .10 .21) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.6,1)]_op{3} .2 .13 .21) (builtin_comp2_func[(.6,1)][(.4~,1) (.5~,1) (.6~,1)]_op{3} .2 .25) (assoc_func[(.8,1)]_op{3} .2 .7 .19) (builtin_comp2_func[(.4,1)][(.8,1)]_op{3} .8 .19) (builtin_assc_func[(.8,1)]_op{3} .6 .5 .19)))] (intch_tgt_op{3} .6 .5 .17)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .10 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .10 .21) (builtin_comp2_op{2} .2 [.22]) (assoc_op{3} .2 .7 .16) (builtin_comp2_op{2} [.8] .16) (builtin_assc_op{3} .6 .5 .16))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .6 [(builtin_comp2_op{2} .5 [.19])])) (intch_tgt_op{3} .6 .5 .17)) (!1builtin_comp3 (intch_src_op{3} .2 .10 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .10 .21) (builtin_comp2_op{2} .2 [.22]) (assoc_op{3} .2 .7 .16) (builtin_comp2_op{2} [.8] .16) (builtin_assc_op{3} .6 .5 .16))) [(intch_tgt_func[(.8,1)]_op{3} .6 .5 .19)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .10 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .10 .21) (builtin_comp2_op{2} .2 [.22]) (assoc_op{3} .2 .7 .16) (builtin_comp2_op{2} [.8] .16) (builtin_assc_op{3} .6 .5 .16))) (intch_tgt_op{3} .6 .5 .16) (builtin_comp2_op{2} .6 [(builtin_comp2_op{2} .5 [.19])])))) (intch_src_op{3} (intch_src_op{3} .2 .10 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .10 .21) (builtin_comp2_op{2} .2 [.22]) (assoc_op{3} .2 .7 .16) (builtin_comp2_op{2} [.8] .16) (builtin_assc_op{3} .6 .5 .16))) (intch_tgt_op{3} .6 .5 .16) (builtin_comp2_op{2} .6 [(builtin_comp2_op{2} .5 [.19])])))) -> (!2builtin_comp2 (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} .2 [.12])] .21) (intch_src_op{3} .2 .11 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .11 .21) (builtin_comp2_op{2} .2 [.23]) (assoc_op{3} .2 .7 .17) (builtin_comp2_op{2} [.8] .17) (builtin_assc_op{3} .6 .5 .17))) (intch_tgt_op{3} .6 .5 .17)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} .2 [.12])] .21) (intch_src_op{3} .2 .11 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .11 .21) (builtin_comp2_op{2} .2 [.23]) (assoc_op{3} .2 .7 .17) (builtin_comp2_op{2} [.8] .17) (builtin_assc_op{3} .6 .5 .17))) (intch_tgt_op{3} .6 .5 .17)) (!1builtin_comp3 [(intch_src_func[(.6,1)]_op{3} .2 .12 .21)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .11 .21) (builtin_comp2_op{2} .2 [.23]) (assoc_op{3} .2 .7 .17) (builtin_comp2_op{2} [.8] .17) (builtin_assc_op{3} .6 .5 .17))) (intch_tgt_op{3} .6 .5 .17)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .10 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} .2 [.12])] .21)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .11 .21) (builtin_comp2_op{2} .2 [.23]) (assoc_op{3} .2 .7 .17) (builtin_comp2_op{2} [.8] .17) (builtin_assc_op{3} .6 .5 .17))) (intch_tgt_op{3} .6 .5 .17)) (!1builtin_comp3 (intch_src_op{3} .2 .10 .21) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.6,1)]_op{3} .2 .12 .21) (builtin_comp2_func[(.6,1)][(.4~,1) (.5~,1) (.6~,1)]_op{3} .2 .24) (assoc_func[(.8,1)]_op{3} .2 .7 .18) (builtin_comp2_func[(.4,1)][(.8,1)]_op{3} .8 .18) (builtin_assc_func[(.8,1)]_op{3} .6 .5 .18)))] (intch_tgt_op{3} .6 .5 .17)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .10 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .10 .21) (builtin_comp2_op{2} .2 [.22]) (assoc_op{3} .2 .7 .16) (builtin_comp2_op{2} [.8] .16) (builtin_assc_op{3} .6 .5 .16))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .6 [(builtin_comp2_op{2} .5 [.18])])) (intch_tgt_op{3} .6 .5 .17)) (!1builtin_comp3 (intch_src_op{3} .2 .10 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .10 .21) (builtin_comp2_op{2} .2 [.22]) (assoc_op{3} .2 .7 .16) (builtin_comp2_op{2} [.8] .16) (builtin_assc_op{3} .6 .5 .16))) [(intch_tgt_func[(.8,1)]_op{3} .6 .5 .18)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .10 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .10 .21) (builtin_comp2_op{2} .2 [.22]) (assoc_op{3} .2 .7 .16) (builtin_comp2_op{2} [.8] .16) (builtin_assc_op{3} .6 .5 .16))) (intch_tgt_op{3} .6 .5 .16) (builtin_comp2_op{2} .6 [(builtin_comp2_op{2} .5 [.18])])))) (intch_src_op{3} (intch_src_op{3} .2 .10 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .10 .21) (builtin_comp2_op{2} .2 [.22]) (assoc_op{3} .2 .7 .16) (builtin_comp2_op{2} [.8] .16) (builtin_assc_op{3} .6 .5 .16))) (intch_tgt_op{3} .6 .5 .16) (builtin_comp2_op{2} .6 [(builtin_comp2_op{2} .5 [.18])]))) (!1builtin_comp2 (!1builtin_comp3 (intch_src_op{3} .2 .10 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .10 .21) (builtin_comp2_op{2} .2 [.22]) (assoc_op{3} .2 .7 .16) (builtin_comp2_op{2} [.8] .16) (builtin_assc_op{3} .6 .5 .16))) (intch_tgt_op{3} .6 .5 .16)) [(builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .6 (builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .5 .20))])).
+  [=^.^=] check cylcomp(3,1,4)
+  [=I.I=] valid term builtin_conecomp(2,1,2)_func[(.26,1) (.22,1) (.18,1) (.14,1) (.9,1) (.4,1)]_op{3}_func[(.32,1) (.26,1) (.20,1)]_op{4} of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} (builtin_comp2_func[(.6,1)]_red_func[(.10,1)]_op{3} .4 .20) .27)] (!1builtin_comp3 (intch_src_op{3} .3 .17 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .17 .27) (builtin_comp2_op{2} .3 [.29]) (assoc_op{3} .3 .11 .23) (builtin_comp2_op{2} [.13] .23) (builtin_assc_op{3} .10 .8 .23))) (intch_tgt_op{3} .10 .8 .23))) (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .19)] .27) (intch_src_op{3} .3 .17 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .17 .27) (builtin_comp2_op{2} .3 [.29]) (assoc_op{3} .3 .11 .23) (builtin_comp2_op{2} [.13] .23) (builtin_assc_op{3} .10 .8 .23))) (intch_tgt_op{3} .10 .8 .23)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .19)] .27) (intch_src_op{3} .3 .17 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .17 .27) (builtin_comp2_op{2} .3 [.29]) (assoc_op{3} .3 .11 .23) (builtin_comp2_op{2} [.13] .23) (builtin_assc_op{3} .10 .8 .23))) (intch_tgt_op{3} .10 .8 .23)) (!1builtin_comp3 [(intch_src_func[(.4,1) (.8,1)]_op{3} .4 .19 .27)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .17 .27) (builtin_comp2_op{2} .3 [.29]) (assoc_op{3} .3 .11 .23) (builtin_comp2_op{2} [.13] .23) (builtin_assc_op{3} .10 .8 .23))) (intch_tgt_op{3} .10 .8 .23)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .16 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .19)] .27)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .17 .27) (builtin_comp2_op{2} .3 [.29]) (assoc_op{3} .3 .11 .23) (builtin_comp2_op{2} [.13] .23) (builtin_assc_op{3} .10 .8 .23))) (intch_tgt_op{3} .10 .8 .23)) (!1builtin_comp3 (intch_src_op{3} .2 .16 .27) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.4,1) (.8,1)]_op{3} .4 .19 .27) (builtin_comp2_func[(.6,1)][(.2~,1) (.4~,1) (.5~,1) (.6~,1)]_op{3} .4 .31) (assoc_func[(.4,1) (.10,1)]_op{3} .4 .11 .25) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1) (.6~,1)]_op{3} .14 .25) (builtin_assc_func[(.6,1) (.10,1)]_op{3} .10 .9 .25)))] (intch_tgt_op{3} .10 .8 .23)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .16 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .27) (builtin_comp2_op{2} .2 [.28]) (assoc_op{3} .2 .11 .22) (builtin_comp2_op{2} [.12] .22) (builtin_assc_op{3} .10 .7 .22))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .10 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .9 .25)])) (intch_tgt_op{3} .10 .8 .23)) (!1builtin_comp3 (intch_src_op{3} .2 .16 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .27) (builtin_comp2_op{2} .2 [.28]) (assoc_op{3} .2 .11 .22) (builtin_comp2_op{2} [.12] .22) (builtin_assc_op{3} .10 .7 .22))) [(intch_tgt_func[(.6,1) (.10,1)]_op{3} .10 .9 .25)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .16 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .27) (builtin_comp2_op{2} .2 [.28]) (assoc_op{3} .2 .11 .22) (builtin_comp2_op{2} [.12] .22) (builtin_assc_op{3} .10 .7 .22))) (intch_tgt_op{3} .10 .7 .22) (builtin_comp2_op{2} .10 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .9 .25)])))) (intch_src_op{3} (intch_src_op{3} .2 .16 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .27) (builtin_comp2_op{2} .2 [.28]) (assoc_op{3} .2 .11 .22) (builtin_comp2_op{2} [.12] .22) (builtin_assc_op{3} .10 .7 .22))) (intch_tgt_op{3} .10 .7 .22) (builtin_comp2_op{2} .10 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .9 .25)])))) -> (!2builtin_comp2 (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .18)] .27) (intch_src_op{3} .3 .17 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .17 .27) (builtin_comp2_op{2} .3 [.29]) (assoc_op{3} .3 .11 .23) (builtin_comp2_op{2} [.13] .23) (builtin_assc_op{3} .10 .8 .23))) (intch_tgt_op{3} .10 .8 .23)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .18)] .27) (intch_src_op{3} .3 .17 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .17 .27) (builtin_comp2_op{2} .3 [.29]) (assoc_op{3} .3 .11 .23) (builtin_comp2_op{2} [.13] .23) (builtin_assc_op{3} .10 .8 .23))) (intch_tgt_op{3} .10 .8 .23)) (!1builtin_comp3 [(intch_src_func[(.4,1) (.8,1)]_op{3} .4 .18 .27)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .17 .27) (builtin_comp2_op{2} .3 [.29]) (assoc_op{3} .3 .11 .23) (builtin_comp2_op{2} [.13] .23) (builtin_assc_op{3} .10 .8 .23))) (intch_tgt_op{3} .10 .8 .23)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .16 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .18)] .27)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .17 .27) (builtin_comp2_op{2} .3 [.29]) (assoc_op{3} .3 .11 .23) (builtin_comp2_op{2} [.13] .23) (builtin_assc_op{3} .10 .8 .23))) (intch_tgt_op{3} .10 .8 .23)) (!1builtin_comp3 (intch_src_op{3} .2 .16 .27) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.4,1) (.8,1)]_op{3} .4 .18 .27) (builtin_comp2_func[(.6,1)][(.2~,1) (.4~,1) (.5~,1) (.6~,1)]_op{3} .4 .30) (assoc_func[(.4,1) (.10,1)]_op{3} .4 .11 .24) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1) (.6~,1)]_op{3} .14 .24) (builtin_assc_func[(.6,1) (.10,1)]_op{3} .10 .9 .24)))] (intch_tgt_op{3} .10 .8 .23)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .16 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .27) (builtin_comp2_op{2} .2 [.28]) (assoc_op{3} .2 .11 .22) (builtin_comp2_op{2} [.12] .22) (builtin_assc_op{3} .10 .7 .22))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .10 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .9 .24)])) (intch_tgt_op{3} .10 .8 .23)) (!1builtin_comp3 (intch_src_op{3} .2 .16 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .27) (builtin_comp2_op{2} .2 [.28]) (assoc_op{3} .2 .11 .22) (builtin_comp2_op{2} [.12] .22) (builtin_assc_op{3} .10 .7 .22))) [(intch_tgt_func[(.6,1) (.10,1)]_op{3} .10 .9 .24)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .16 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .27) (builtin_comp2_op{2} .2 [.28]) (assoc_op{3} .2 .11 .22) (builtin_comp2_op{2} [.12] .22) (builtin_assc_op{3} .10 .7 .22))) (intch_tgt_op{3} .10 .7 .22) (builtin_comp2_op{2} .10 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .9 .24)])))) (intch_src_op{3} (intch_src_op{3} .2 .16 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .27) (builtin_comp2_op{2} .2 [.28]) (assoc_op{3} .2 .11 .22) (builtin_comp2_op{2} [.12] .22) (builtin_assc_op{3} .10 .7 .22))) (intch_tgt_op{3} .10 .7 .22) (builtin_comp2_op{2} .10 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .9 .24)]))) (!1builtin_comp2 (!1builtin_comp3 (intch_src_op{3} .2 .16 .27) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .27) (builtin_comp2_op{2} .2 [.28]) (assoc_op{3} .2 .11 .22) (builtin_comp2_op{2} [.12] .22) (builtin_assc_op{3} .10 .7 .22))) (intch_tgt_op{3} .10 .7 .22)) [(builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .10 (builtin_comp2_func[(.6,1)]_red_func[(.10,1)]_op{3} .9 .26))])).
+  [=^.^=] check cylcomp(4,2,3)
+  [=I.I=] valid term builtin_conecomp(3,2,3)_func[(.20,1) (.13,1) (.6,1)]_op{4} of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} (!1builtin_comp2 [.6] .22) .15)] .25) (!2builtin_comp3 (!1builtin_comp2 [(builtin_comp_1_0_intch_op{4} .5 .22 .15)] .25) (!2builtin_comp3 (!1intch_src (builtin_comp2_op{2} [.5] .15) (builtin_comp2_op{2} [.22] .15) .25) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp5 (!1builtin_assc (builtin_comp2_op{2} [.5] .15) (builtin_comp2_op{2} [.22] .15) .25) (!1builtin_comp2 (builtin_comp2_op{2} [.5] .15) [.26]) (!1assoc (builtin_comp2_op{2} [.5] .15) .17 (builtin_comp2_op{2} .14 [.24])) (!1builtin_comp2 [.19] (builtin_comp2_op{2} .14 [.24])) (!1builtin_assc .16 (builtin_comp2_op{2} .14 [.12]) (builtin_comp2_op{2} .14 [.24])))) (!1intch_tgt .16 (builtin_comp2_op{2} .14 [.12]) (builtin_comp2_op{2} .14 [.24]))) (!1builtin_comp2 .16 [(builtin_comp_1_0_intch_op{1}^-1 .14 .12 .24)]))) -> (!2builtin_comp2 (!2builtin_comp3 (!1builtin_comp2 [(builtin_comp_1_0_intch_op{4} .4 .22 .15)] .25) (!2builtin_comp3 (!1intch_src (builtin_comp2_op{2} [.4] .15) (builtin_comp2_op{2} [.22] .15) .25) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp5 (!1builtin_assc (builtin_comp2_op{2} [.4] .15) (builtin_comp2_op{2} [.22] .15) .25) (!1builtin_comp2 (builtin_comp2_op{2} [.4] .15) [.26]) (!1assoc (builtin_comp2_op{2} [.4] .15) .17 (builtin_comp2_op{2} .14 [.24])) (!1builtin_comp2 [.18] (builtin_comp2_op{2} .14 [.24])) (!1builtin_assc .16 (builtin_comp2_op{2} .14 [.11]) (builtin_comp2_op{2} .14 [.24])))) (!1intch_tgt .16 (builtin_comp2_op{2} .14 [.11]) (builtin_comp2_op{2} .14 [.24]))) (!1builtin_comp2 .16 [(builtin_comp_1_0_intch_op{1}^-1 .14 .11 .24)])) (!1builtin_comp2 .16 [(builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .14 (!1builtin_comp2 [.13] .24))])).
+  [=^.^=] check cylcomp(3,2,4)
+  [=I.I=] valid term builtin_conecomp(3,2,3)_func[(.26,1) (.22,1) (.18,1)]_op{4} of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} (!1builtin_comp2 .4 [.18]) .11)] .23) (!2builtin_comp3 (!1builtin_comp2 [(builtin_comp_1_0_intch_op{4} .4 .17 .11)] .23) (!2builtin_comp3 (!1intch_src (builtin_comp2_op{2} [.4] .11) (builtin_comp2_op{2} [.17] .11) .23) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp5 (!1builtin_assc (builtin_comp2_op{2} [.4] .11) (builtin_comp2_op{2} [.17] .11) .23) (!1builtin_comp2 (builtin_comp2_op{2} [.4] .11) [.25]) (!1assoc (builtin_comp2_op{2} [.4] .11) .13 (builtin_comp2_op{2} .10 [.21])) (!1builtin_comp2 [.14] (builtin_comp2_op{2} .10 [.21])) (!1builtin_assc .12 (builtin_comp2_op{2} .10 [.9]) (builtin_comp2_op{2} .10 [.21])))) (!1intch_tgt .12 (builtin_comp2_op{2} .10 [.9]) (builtin_comp2_op{2} .10 [.21]))) (!1builtin_comp2 .12 [(builtin_comp_1_0_intch_op{1}^-1 .10 .9 .21)]))) -> (!2builtin_comp2 (!2builtin_comp3 (!1builtin_comp2 [(builtin_comp_1_0_intch_op{4} .4 .16 .11)] .23) (!2builtin_comp3 (!1intch_src (builtin_comp2_op{2} [.4] .11) (builtin_comp2_op{2} [.16] .11) .23) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp5 (!1builtin_assc (builtin_comp2_op{2} [.4] .11) (builtin_comp2_op{2} [.16] .11) .23) (!1builtin_comp2 (builtin_comp2_op{2} [.4] .11) [.24]) (!1assoc (builtin_comp2_op{2} [.4] .11) .13 (builtin_comp2_op{2} .10 [.20])) (!1builtin_comp2 [.14] (builtin_comp2_op{2} .10 [.20])) (!1builtin_assc .12 (builtin_comp2_op{2} .10 [.9]) (builtin_comp2_op{2} .10 [.20])))) (!1intch_tgt .12 (builtin_comp2_op{2} .10 [.9]) (builtin_comp2_op{2} .10 [.20]))) (!1builtin_comp2 .12 [(builtin_comp_1_0_intch_op{1}^-1 .10 .9 .20)])) (!1builtin_comp2 .12 [(builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .10 (!1builtin_comp2 .9 [.22]))])).
+  [=^.^=] check cylstack(2)
+  [=I.I=] valid term builtin_cylstack of type (builtin_comp2_op{2} .2 (builtin_comp2_op{2} .7 .13)) -> (builtin_comp2_op{2} (builtin_comp2_op{2} .6 .12) .11).
+  [=^.^=] check cylstack(3)
+  [=I.I=] valid term builtin_cylstack_func[(.24,1) (.19,1) (.14,1) (.9,1) (.4,1)]_op{3} of type (!1builtin_comp2 (builtin_comp2_op{2} [.4] (builtin_comp2_op{2} .11 .21)) (!1builtin_comp3 (intch_tgt_op{2} .3 .11 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .3 .11 .21) (builtin_comp2_op{2} [.13] .21) (builtin_assc_op{3} .10 .8 .21) (builtin_comp2_op{2} .10 [.23]) (assoc_op{3} .10 .20 .18))) (intch_src_op{2} .10 .20 .18))) -> (!1builtin_comp2 (!1builtin_comp3 (intch_tgt_op{2} .2 .11 .21) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .2 .11 .21) (builtin_comp2_op{2} [.12] .21) (builtin_assc_op{3} .10 .7 .21) (builtin_comp2_op{2} .10 [.22]) (assoc_op{3} .10 .20 .17))) (intch_src_op{2} .10 .20 .17)) (builtin_comp2_op{2} (builtin_comp2_op{2} .10 .20) [.19])).
+  [=^.^=] check cylstack(4)
+  [=I.I=] valid term builtin_cylstack_func[(.24,1) (.19,1) (.14,1) (.9,1) (.4,1)]_op{3}_func[(.34,1) (.27,1) (.20,1) (.13,1) (.6,1)]_op{4} of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} .6 (builtin_comp2_op{2} .15 .29))] (!1builtin_comp3 (intch_tgt_op{2} .3 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29) (builtin_comp2_op{2} .14 [.31]) (assoc_op{3} .14 .28 .24))) (intch_src_op{2} .14 .28 .24))) (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [.5] (builtin_comp2_op{2} .15 .29)) (intch_tgt_op{2} .3 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29) (builtin_comp2_op{2} .14 [.31]) (assoc_op{3} .14 .28 .24))) (intch_src_op{2} .14 .28 .24)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [.5] (builtin_comp2_op{2} .15 .29)) (intch_tgt_op{2} .3 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29) (builtin_comp2_op{2} .14 [.31]) (assoc_op{3} .14 .28 .24))) (intch_src_op{2} .14 .28 .24)) (!1builtin_comp3 [(intch_tgt_op{2}_func[(.4,1)]_op{3} .5 .15 .29)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29) (builtin_comp2_op{2} .14 [.31]) (assoc_op{3} .14 .28 .24))) (intch_src_op{2} .14 .28 .24)) (!1builtin_assc_op{3} (intch_tgt_op{2} .2 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [.5] (builtin_comp2_op{2} .15 .29))) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29) (builtin_comp2_op{2} .14 [.31]) (assoc_op{3} .14 .28 .24))) (intch_src_op{2} .14 .28 .24)) (!1builtin_comp3 (intch_tgt_op{2} .2 .15 .29) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (assoc_func[(.4,1)]_op{3} .5 .15 .29) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} .19 .29) (builtin_assc_func[(.6,1)]_op{3} .14 .12 .29) (builtin_comp2_func[(.6,1)][(.4~,1) (.5~,1) (.6~,1)]_op{3} .14 .33) (assoc_func[(.8,1)]_op{3} .14 .28 .26)))] (intch_src_op{2} .14 .28 .24)) (!1builtin_assc_op{3} (intch_tgt_op{2} .2 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .2 .15 .29) (builtin_comp2_op{2} [.16] .29) (builtin_assc_op{3} .14 .9 .29) (builtin_comp2_op{2} .14 [.30]) (assoc_op{3} .14 .28 .23))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} (builtin_comp2_op{2} .14 .28) [.26])) (intch_src_op{2} .14 .28 .24)) (!1builtin_comp3 (intch_tgt_op{2} .2 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .2 .15 .29) (builtin_comp2_op{2} [.16] .29) (builtin_assc_op{3} .14 .9 .29) (builtin_comp2_op{2} .14 [.30]) (assoc_op{3} .14 .28 .23))) [(intch_src_op{2}_func[(.8,1)]_op{3} .14 .28 .26)]) (!1builtin_assc_op{3} (intch_tgt_op{2} .2 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .2 .15 .29) (builtin_comp2_op{2} [.16] .29) (builtin_assc_op{3} .14 .9 .29) (builtin_comp2_op{2} .14 [.30]) (assoc_op{3} .14 .28 .23))) (intch_src_op{2} .14 .28 .23) (builtin_comp2_op{2} (builtin_comp2_op{2} .14 .28) [.26])))) (intch_src_op{3} (intch_tgt_op{2} .2 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .2 .15 .29) (builtin_comp2_op{2} [.16] .29) (builtin_assc_op{3} .14 .9 .29) (builtin_comp2_op{2} .14 [.30]) (assoc_op{3} .14 .28 .23))) (intch_src_op{2} .14 .28 .23) (builtin_comp2_op{2} (builtin_comp2_op{2} .14 .28) [.26])))) -> (!2builtin_comp2 (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [.4] (builtin_comp2_op{2} .15 .29)) (intch_tgt_op{2} .3 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29) (builtin_comp2_op{2} .14 [.31]) (assoc_op{3} .14 .28 .24))) (intch_src_op{2} .14 .28 .24)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [.4] (builtin_comp2_op{2} .15 .29)) (intch_tgt_op{2} .3 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29) (builtin_comp2_op{2} .14 [.31]) (assoc_op{3} .14 .28 .24))) (intch_src_op{2} .14 .28 .24)) (!1builtin_comp3 [(intch_tgt_op{2}_func[(.4,1)]_op{3} .4 .15 .29)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29) (builtin_comp2_op{2} .14 [.31]) (assoc_op{3} .14 .28 .24))) (intch_src_op{2} .14 .28 .24)) (!1builtin_assc_op{3} (intch_tgt_op{2} .2 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [.4] (builtin_comp2_op{2} .15 .29))) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .3 .15 .29) (builtin_comp2_op{2} [.17] .29) (builtin_assc_op{3} .14 .10 .29) (builtin_comp2_op{2} .14 [.31]) (assoc_op{3} .14 .28 .24))) (intch_src_op{2} .14 .28 .24)) (!1builtin_comp3 (intch_tgt_op{2} .2 .15 .29) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (assoc_func[(.4,1)]_op{3} .4 .15 .29) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} .18 .29) (builtin_assc_func[(.6,1)]_op{3} .14 .11 .29) (builtin_comp2_func[(.6,1)][(.4~,1) (.5~,1) (.6~,1)]_op{3} .14 .32) (assoc_func[(.8,1)]_op{3} .14 .28 .25)))] (intch_src_op{2} .14 .28 .24)) (!1builtin_assc_op{3} (intch_tgt_op{2} .2 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .2 .15 .29) (builtin_comp2_op{2} [.16] .29) (builtin_assc_op{3} .14 .9 .29) (builtin_comp2_op{2} .14 [.30]) (assoc_op{3} .14 .28 .23))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} (builtin_comp2_op{2} .14 .28) [.25])) (intch_src_op{2} .14 .28 .24)) (!1builtin_comp3 (intch_tgt_op{2} .2 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .2 .15 .29) (builtin_comp2_op{2} [.16] .29) (builtin_assc_op{3} .14 .9 .29) (builtin_comp2_op{2} .14 [.30]) (assoc_op{3} .14 .28 .23))) [(intch_src_op{2}_func[(.8,1)]_op{3} .14 .28 .25)]) (!1builtin_assc_op{3} (intch_tgt_op{2} .2 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .2 .15 .29) (builtin_comp2_op{2} [.16] .29) (builtin_assc_op{3} .14 .9 .29) (builtin_comp2_op{2} .14 [.30]) (assoc_op{3} .14 .28 .23))) (intch_src_op{2} .14 .28 .23) (builtin_comp2_op{2} (builtin_comp2_op{2} .14 .28) [.25])))) (intch_src_op{3} (intch_tgt_op{2} .2 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .2 .15 .29) (builtin_comp2_op{2} [.16] .29) (builtin_assc_op{3} .14 .9 .29) (builtin_comp2_op{2} .14 [.30]) (assoc_op{3} .14 .28 .23))) (intch_src_op{2} .14 .28 .23) (builtin_comp2_op{2} (builtin_comp2_op{2} .14 .28) [.25]))) (!1builtin_comp2 (!1builtin_comp3 (intch_tgt_op{2} .2 .15 .29) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (assoc_op{3} .2 .15 .29) (builtin_comp2_op{2} [.16] .29) (builtin_assc_op{3} .14 .9 .29) (builtin_comp2_op{2} .14 [.30]) (assoc_op{3} .14 .28 .23))) (intch_src_op{2} .14 .28 .23)) [(builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} (builtin_comp2_op{2} .14 .28) .27)])).
+
+  $ catt --no-builtins features/eh.catt
+  [=^.^=] check eh^2_(0,1)
+  [=I.I=] valid term eh^2_(0,1) of type (builtin_comp2 [.1] [.2]) -> (!1builtin_comp3 (UBPad.p(1) .0) (!1builtin_comp2 .1 .2) (UBPad.p(1) .0)).
+  [=^.^=] check eh^3_(0,1)
+  [=I.I=] valid term eh^3_(0,1) of type (builtin_comp2 [[.1]] [[.2]]) -> (!2builtin_comp3 (UBPad.p(2) .0) (UBPad.Padding(2) [(!1builtin_comp2 [.1] [.2])]) (UBPad.p(2) .0)).
+  [=^.^=] check eh^4_(2,1)
+  [=I.I=] valid term eh^4_(2,1) of type (!2builtin_comp2 [.1] [.2]) -> (!3builtin_comp3 (UBPad.p(3) .0) (UBPad.Padding(3) [(!1builtin_comp2 [[.1]] [[.2]])]) (UBPad.p(3) .0)).
+  [=^.^=] check eh^3_(1,2)
+  [=I.I=] valid term eh^3_(1,2) of type (!1builtin_comp2 [.1] [.2]) -> (!2builtin_comp3 (UBPad.p(2) .0) (!2builtin_comp2 .1 .2) (UBPad.p(2) .0)).
+  [=^.^=] check eh^4_(3,2)
+  [=I.I=] valid term eh^4_(3,2) of type (!3builtin_comp2 .1 .2) -> (!3builtin_comp3 (UBPad.p(3) .0) (!2builtin_comp2 [.1] [.2]) (UBPad.p(3) .0)).
+  [=^.^=] check eh^3_(1,2)
+  [=I.I=] valid term eh^3_(1,2) of type (!1builtin_comp2 [.1] [.2]) -> (!2builtin_comp3 (UBPad.p(2) .0) (!2builtin_comp2 .1 .2) (UBPad.p(2) .0)).
+  [=^.^=] check eh^4_(2,3)
+  [=I.I=] valid term eh^4_(2,3) of type (!2builtin_comp2 [.1] [.2]) -> (!3builtin_comp3 (UBPad.p(3) .0) (!3builtin_comp2 .1 .2) (UBPad.p(3) .0)).
+  [=^.^=] check eh^3_(0,2)
+  [=I.I=] valid term eh^3_(0,2) of type (builtin_comp2 [[.1]] [[.2]]) -> (!2builtin_comp3 (UBPad.p(2) .0) (!1builtin_comp3 (UBPad.p(1) .0) [(!2builtin_comp2 .1 .2)] (UBPad.p(1) .0)) (UBPad.p(2) .0)).
+  [=^.^=] check eh^2_(1,0)
+  [=I.I=] valid term eh^2_(1,0) of type (!1builtin_comp2 .1 .2) -> (!1builtin_comp3 (UBPad.p(1) .0) (builtin_comp2 [.1] [.2]) (UBPad.p(1) .0)).
+  [=^.^=] check eh^3_(2,0)
+  [=I.I=] valid term eh^3_(2,0) of type (!2builtin_comp2 .1 .2) -> (!2builtin_comp3 (UBPad.p(2) .0) (!1builtin_comp3 (UBPad.p(1) .0) [(builtin_comp2 [[.1]] [[.2]])] (UBPad.p(1) .0)) (UBPad.p(2) .0)).
+  [=^.^=] check EH^2_(0,1)
+  [=I.I=] valid term (!2builtin_comp2 (eh^2_(0,1) .1 .2) (I(eh^2_(0,1)_op{2}) .2 .1)) of type (builtin_comp2 [.1] [.2]) -> (builtin_comp2_func[(.4,1) (.8,1)]_op{2} .2 .1).
+  [=^.^=] check EH^3_(0,1)
+  [=I.I=] valid term (!3builtin_comp2 (eh^3_(0,1) .1 .2) (I(eh^3_(0,1)_op{2}) .2 .1)) of type (builtin_comp2 [[.1]] [[.2]]) -> (builtin_comp2_func[(.6,2) (.12,2)]_op{2} .2 .1).
+  [=^.^=] check EH^3_(1,2)
+  [=I.I=] valid term (!3builtin_comp2 (eh^3_(1,2) .1 .2) (I(eh^3_(1,2)_op{3}) .2 .1)) of type (!1builtin_comp2 [.1] [.2]) -> (!1builtin_comp2_func[(.6,1) (.10,1)]_op{3} .2 .1).
+  [=^.^=] check EH^3_(1,2)
+  [=I.I=] valid term (!3builtin_comp2 (eh^3_(1,2) .1 .2) (I(eh^3_(1,2)_op{3}) .2 .1)) of type (!1builtin_comp2 [.1] [.2]) -> (!1builtin_comp2_func[(.6,1) (.10,1)]_op{3} .2 .1).
+  [=^.^=] check EH^3_(2,0)
+  [=I.I=] valid term (!3builtin_comp2 (eh^3_(2,0) .1 .2) (I(eh^3_(2,0)_op{1}) .2 .1)) of type (!2builtin_comp2 .1 .2) -> (!2builtin_comp2 .2 .1).