-(CHead c0 k u1) (let H7 \def (match H4 in pr2 return (\lambda (c: C).(\lambda
-(t: T).(\lambda (t5: T).(\lambda (_: (pr2 c t t5)).((eq C c (CHead c3 k u1))
-\to ((eq T t t3) \to ((eq T t5 t0) \to (pr3 (CHead c0 k u1) t3 t0))))))))
-with [(pr2_free c t5 t6 H7) \Rightarrow (\lambda (H8: (eq C c (CHead c3 k
-u1))).(\lambda (H9: (eq T t5 t3)).(\lambda (H10: (eq T t6 t0)).(eq_ind C
-(CHead c3 k u1) (\lambda (_: C).((eq T t5 t3) \to ((eq T t6 t0) \to ((pr0 t5
-t6) \to (pr3 (CHead c0 k u1) t3 t0))))) (\lambda (H11: (eq T t5 t3)).(eq_ind
-T t3 (\lambda (t: T).((eq T t6 t0) \to ((pr0 t t6) \to (pr3 (CHead c0 k u1)
-t3 t0)))) (\lambda (H12: (eq T t6 t0)).(eq_ind T t0 (\lambda (t: T).((pr0 t3
-t) \to (pr3 (CHead c0 k u1) t3 t0))) (\lambda (H13: (pr0 t3 t0)).(pr3_pr2
-(CHead c0 k u1) t3 t0 (pr2_free (CHead c0 k u1) t3 t0 H13))) t6 (sym_eq T t6
-t0 H12))) t5 (sym_eq T t5 t3 H11))) c (sym_eq C c (CHead c3 k u1) H8) H9 H10
-H7)))) | (pr2_delta c d u i H7 t5 t6 H8 t H9) \Rightarrow (\lambda (H10: (eq
-C c (CHead c3 k u1))).(\lambda (H11: (eq T t5 t3)).(\lambda (H12: (eq T t
-t0)).(eq_ind C (CHead c3 k u1) (\lambda (c4: C).((eq T t5 t3) \to ((eq T t
-t0) \to ((getl i c4 (CHead d (Bind Abbr) u)) \to ((pr0 t5 t6) \to ((subst0 i
-u t6 t) \to (pr3 (CHead c0 k u1) t3 t0))))))) (\lambda (H13: (eq T t5
-t3)).(eq_ind T t3 (\lambda (t7: T).((eq T t t0) \to ((getl i (CHead c3 k u1)
-(CHead d (Bind Abbr) u)) \to ((pr0 t7 t6) \to ((subst0 i u t6 t) \to (pr3
-(CHead c0 k u1) t3 t0)))))) (\lambda (H14: (eq T t t0)).(eq_ind T t0 (\lambda
-(t7: T).((getl i (CHead c3 k u1) (CHead d (Bind Abbr) u)) \to ((pr0 t3 t6)
-\to ((subst0 i u t6 t7) \to (pr3 (CHead c0 k u1) t3 t0))))) (\lambda (H15:
-(getl i (CHead c3 k u1) (CHead d (Bind Abbr) u))).(\lambda (H16: (pr0 t3
-t6)).(\lambda (H17: (subst0 i u t6 t0)).(ex3_2_ind C T (\lambda (e2:
+(CHead c0 k u1) (insert_eq C (CHead c3 k u1) (\lambda (c: C).(pr2 c t3 t0))
+(\lambda (_: C).(pr3 (CHead c0 k u1) t3 t0)) (\lambda (y: C).(\lambda (H7:
+(pr2 y t3 t0)).(pr2_ind (\lambda (c: C).(\lambda (t: T).(\lambda (t5: T).((eq
+C c (CHead c3 k u1)) \to (pr3 (CHead c0 k u1) t t5))))) (\lambda (c:
+C).(\lambda (t5: T).(\lambda (t6: T).(\lambda (H8: (pr0 t5 t6)).(\lambda (_:
+(eq C c (CHead c3 k u1))).(pr3_pr2 (CHead c0 k u1) t5 t6 (pr2_free (CHead c0
+k u1) t5 t6 H8))))))) (\lambda (c: C).(\lambda (d: C).(\lambda (u:
+T).(\lambda (i: nat).(\lambda (H8: (getl i c (CHead d (Bind Abbr)
+u))).(\lambda (t5: T).(\lambda (t6: T).(\lambda (H9: (pr0 t5 t6)).(\lambda
+(t: T).(\lambda (H10: (subst0 i u t6 t)).(\lambda (H11: (eq C c (CHead c3 k
+u1))).(let H12 \def (eq_ind C c (\lambda (c4: C).(getl i c4 (CHead d (Bind
+Abbr) u))) H8 (CHead c3 k u1) H11) in (ex3_2_ind C T (\lambda (e2: