-T).(\lambda (H0: (pr2 c t1 t2)).(let H1 \def (match H0 in pr2 return (\lambda
-(c0: C).(\lambda (t: T).(\lambda (t0: T).(\lambda (_: (pr2 c0 t t0)).((eq C
-c0 c) \to ((eq T t t1) \to ((eq T t0 t2) \to (\forall (w1: T).((subst1 i v t1
-w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v
-t2 w2)))))))))))) with [(pr2_free c0 t0 t3 H1) \Rightarrow (\lambda (H2: (eq
-C c0 c)).(\lambda (H3: (eq T t0 t1)).(\lambda (H4: (eq T t3 t2)).(eq_ind C c
-(\lambda (_: C).((eq T t0 t1) \to ((eq T t3 t2) \to ((pr0 t0 t3) \to (\forall
-(w1: T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2))
-(\lambda (w2: T).(subst1 i v t2 w2))))))))) (\lambda (H5: (eq T t0
-t1)).(eq_ind T t1 (\lambda (t: T).((eq T t3 t2) \to ((pr0 t t3) \to (\forall
-(w1: T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2))
-(\lambda (w2: T).(subst1 i v t2 w2)))))))) (\lambda (H6: (eq T t3
-t2)).(eq_ind T t2 (\lambda (t: T).((pr0 t1 t) \to (\forall (w1: T).((subst1 i
-v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1
-i v t2 w2))))))) (\lambda (H7: (pr0 t1 t2)).(\lambda (w1: T).(\lambda (H8:
-(subst1 i v t1 w1)).(ex2_ind T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2:
-T).(subst1 i v t2 w2)) (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2:
-T).(subst1 i v t2 w2))) (\lambda (x: T).(\lambda (H9: (pr0 w1 x)).(\lambda
-(H10: (subst1 i v t2 x)).(ex_intro2 T (\lambda (w2: T).(pr2 c w1 w2))
-(\lambda (w2: T).(subst1 i v t2 w2)) x (pr2_free c w1 x H9) H10))))
-(pr0_subst1 t1 t2 H7 v w1 i H8 v (pr0_refl v)))))) t3 (sym_eq T t3 t2 H6)))
-t0 (sym_eq T t0 t1 H5))) c0 (sym_eq C c0 c H2) H3 H4 H1)))) | (pr2_delta c0 d
-u i0 H1 t0 t3 H2 t H3) \Rightarrow (\lambda (H4: (eq C c0 c)).(\lambda (H5:
-(eq T t0 t1)).(\lambda (H6: (eq T t t2)).(eq_ind C c (\lambda (c1: C).((eq T
-t0 t1) \to ((eq T t t2) \to ((getl i0 c1 (CHead d (Bind Abbr) u)) \to ((pr0
-t0 t3) \to ((subst0 i0 u t3 t) \to (\forall (w1: T).((subst1 i v t1 w1) \to
-(ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2
-w2))))))))))) (\lambda (H7: (eq T t0 t1)).(eq_ind T t1 (\lambda (t4: T).((eq
-T t t2) \to ((getl i0 c (CHead d (Bind Abbr) u)) \to ((pr0 t4 t3) \to
-((subst0 i0 u t3 t) \to (\forall (w1: T).((subst1 i v t1 w1) \to (ex2 T
-(\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2))))))))))
-(\lambda (H8: (eq T t t2)).(eq_ind T t2 (\lambda (t4: T).((getl i0 c (CHead d
-(Bind Abbr) u)) \to ((pr0 t1 t3) \to ((subst0 i0 u t3 t4) \to (\forall (w1:
-T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda
-(w2: T).(subst1 i v t2 w2))))))))) (\lambda (H9: (getl i0 c (CHead d (Bind
-Abbr) u))).(\lambda (H10: (pr0 t1 t3)).(\lambda (H11: (subst0 i0 u t3
-t2)).(\lambda (w1: T).(\lambda (H12: (subst1 i v t1 w1)).(ex2_ind T (\lambda
-(w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst1 i v t3 w2)) (ex2 T (\lambda
-(w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2))) (\lambda (x:
-T).(\lambda (H13: (pr0 w1 x)).(\lambda (H14: (subst1 i v t3 x)).(neq_eq_e i
-i0 (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2
-w2))) (\lambda (H15: (not (eq nat i i0))).(ex2_ind T (\lambda (t4: T).(subst1
-i v t2 t4)) (\lambda (t4: T).(subst1 i0 u x t4)) (ex2 T (\lambda (w2: T).(pr2
-c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2))) (\lambda (x0: T).(\lambda
-(H16: (subst1 i v t2 x0)).(\lambda (H17: (subst1 i0 u x x0)).(ex_intro2 T
-(\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2)) x0
-(pr2_delta1 c d u i0 H9 w1 x H13 x0 H17) H16)))) (subst1_confluence_neq t3 t2
-u i0 (subst1_single i0 u t3 t2 H11) x v i H14 (sym_not_eq nat i i0 H15))))
-(\lambda (H15: (eq nat i i0)).(let H16 \def (eq_ind_r nat i0 (\lambda (n:
-nat).(subst0 n u t3 t2)) H11 i H15) in (let H17 \def (eq_ind_r nat i0
-(\lambda (n: nat).(getl n c (CHead d (Bind Abbr) u))) H9 i H15) in (let H18
-\def (eq_ind C (CHead e (Bind Abbr) v) (\lambda (c1: C).(getl i c c1)) H
+T).(\lambda (H0: (pr2 c t1 t2)).(insert_eq C c (\lambda (c0: C).(pr2 c0 t1
+t2)) (\lambda (c0: C).(\forall (w1: T).((subst1 i v t1 w1) \to (ex2 T
+(\lambda (w2: T).(pr2 c0 w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2))))))
+(\lambda (y: C).(\lambda (H1: (pr2 y t1 t2)).(pr2_ind (\lambda (c0:
+C).(\lambda (t: T).(\lambda (t0: T).((eq C c0 c) \to (\forall (w1:
+T).((subst1 i v t w1) \to (ex2 T (\lambda (w2: T).(pr2 c0 w1 w2)) (\lambda
+(w2: T).(subst1 i v t0 w2))))))))) (\lambda (c0: C).(\lambda (t3: T).(\lambda
+(t4: T).(\lambda (H2: (pr0 t3 t4)).(\lambda (H3: (eq C c0 c)).(\lambda (w1:
+T).(\lambda (H4: (subst1 i v t3 w1)).(eq_ind_r C c (\lambda (c1: C).(ex2 T
+(\lambda (w2: T).(pr2 c1 w1 w2)) (\lambda (w2: T).(subst1 i v t4 w2))))
+(ex2_ind T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst1 i v t4 w2))
+(ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t4 w2)))
+(\lambda (x: T).(\lambda (H5: (pr0 w1 x)).(\lambda (H6: (subst1 i v t4
+x)).(ex_intro2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v
+t4 w2)) x (pr2_free c w1 x H5) H6)))) (pr0_subst1 t3 t4 H2 v w1 i H4 v
+(pr0_refl v))) c0 H3)))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u:
+T).(\lambda (i0: nat).(\lambda (H2: (getl i0 c0 (CHead d (Bind Abbr)
+u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H3: (pr0 t3 t4)).(\lambda
+(t: T).(\lambda (H4: (subst0 i0 u t4 t)).(\lambda (H5: (eq C c0 c)).(\lambda
+(w1: T).(\lambda (H6: (subst1 i v t3 w1)).(let H7 \def (eq_ind C c0 (\lambda
+(c1: C).(getl i0 c1 (CHead d (Bind Abbr) u))) H2 c H5) in (eq_ind_r C c
+(\lambda (c1: C).(ex2 T (\lambda (w2: T).(pr2 c1 w1 w2)) (\lambda (w2:
+T).(subst1 i v t w2)))) (ex2_ind T (\lambda (w2: T).(pr0 w1 w2)) (\lambda
+(w2: T).(subst1 i v t4 w2)) (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda
+(w2: T).(subst1 i v t w2))) (\lambda (x: T).(\lambda (H8: (pr0 w1
+x)).(\lambda (H9: (subst1 i v t4 x)).(neq_eq_e i i0 (ex2 T (\lambda (w2:
+T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t w2))) (\lambda (H10: (not
+(eq nat i i0))).(ex2_ind T (\lambda (t0: T).(subst1 i v t t0)) (\lambda (t0:
+T).(subst1 i0 u x t0)) (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2:
+T).(subst1 i v t w2))) (\lambda (x0: T).(\lambda (H11: (subst1 i v t
+x0)).(\lambda (H12: (subst1 i0 u x x0)).(ex_intro2 T (\lambda (w2: T).(pr2 c
+w1 w2)) (\lambda (w2: T).(subst1 i v t w2)) x0 (pr2_delta1 c d u i0 H7 w1 x
+H8 x0 H12) H11)))) (subst1_confluence_neq t4 t u i0 (subst1_single i0 u t4 t
+H4) x v i H9 (sym_not_eq nat i i0 H10)))) (\lambda (H10: (eq nat i i0)).(let
+H11 \def (eq_ind_r nat i0 (\lambda (n: nat).(subst0 n u t4 t)) H4 i H10) in
+(let H12 \def (eq_ind_r nat i0 (\lambda (n: nat).(getl n c (CHead d (Bind
+Abbr) u))) H7 i H10) in (let H13 \def (eq_ind C (CHead e (Bind Abbr) v)
+(\lambda (c1: C).(getl i c c1)) H (CHead d (Bind Abbr) u) (getl_mono c (CHead
+e (Bind Abbr) v) i H (CHead d (Bind Abbr) u) H12)) in (let H14 \def (f_equal
+C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with [(CSort _)
+\Rightarrow e | (CHead c1 _ _) \Rightarrow c1])) (CHead e (Bind Abbr) v)