-i u u1 u2)).(insert_eq T u2 (\lambda (t: T).(subst1 i u u1 t)) (ex2 T
-(\lambda (t: T).(subst1 j u1 t1 t)) (\lambda (t: T).(subst1 (S (plus i j)) u
-t t3))) (\lambda (y: T).(\lambda (H2: (subst1 i u u1 y)).(subst1_ind i u u1
-(\lambda (t: T).((eq T t u2) \to (ex2 T (\lambda (t0: T).(subst1 j u1 t1 t0))
-(\lambda (t0: T).(subst1 (S (plus i j)) u t0 t3))))) (\lambda (H3: (eq T u1
-u2)).(eq_ind_r T u2 (\lambda (t: T).(ex2 T (\lambda (t0: T).(subst1 j t t1
-t0)) (\lambda (t0: T).(subst1 (S (plus i j)) u t0 t3)))) (ex_intro2 T
-(\lambda (t: T).(subst1 j u2 t1 t)) (\lambda (t: T).(subst1 (S (plus i j)) u
-t t3)) t3 (subst1_single j u2 t1 t3 H0) (subst1_refl (S (plus i j)) u t3)) u1
-H3)) (\lambda (t0: T).(\lambda (H3: (subst0 i u u1 t0)).(\lambda (H4: (eq T
-t0 u2)).(let H5 \def (eq_ind T t0 (\lambda (t: T).(subst0 i u u1 t)) H3 u2
-H4) in (ex2_ind T (\lambda (t: T).(subst0 j u1 t1 t)) (\lambda (t: T).(subst0
-(S (plus i j)) u t t3)) (ex2 T (\lambda (t: T).(subst1 j u1 t1 t)) (\lambda
-(t: T).(subst1 (S (plus i j)) u t t3))) (\lambda (x: T).(\lambda (H6: (subst0
-j u1 t1 x)).(\lambda (H7: (subst0 (S (plus i j)) u x t3)).(ex_intro2 T
+i u u1 u2)).(insert_eq T u2 (\lambda (t: T).(subst1 i u u1 t)) (\lambda (_:
+T).(ex2 T (\lambda (t0: T).(subst1 j u1 t1 t0)) (\lambda (t0: T).(subst1 (S
+(plus i j)) u t0 t3)))) (\lambda (y: T).(\lambda (H2: (subst1 i u u1
+y)).(subst1_ind i u u1 (\lambda (t: T).((eq T t u2) \to (ex2 T (\lambda (t0:
+T).(subst1 j u1 t1 t0)) (\lambda (t0: T).(subst1 (S (plus i j)) u t0 t3)))))
+(\lambda (H3: (eq T u1 u2)).(eq_ind_r T u2 (\lambda (t: T).(ex2 T (\lambda
+(t0: T).(subst1 j t t1 t0)) (\lambda (t0: T).(subst1 (S (plus i j)) u t0
+t3)))) (ex_intro2 T (\lambda (t: T).(subst1 j u2 t1 t)) (\lambda (t:
+T).(subst1 (S (plus i j)) u t t3)) t3 (subst1_single j u2 t1 t3 H0)
+(subst1_refl (S (plus i j)) u t3)) u1 H3)) (\lambda (t0: T).(\lambda (H3:
+(subst0 i u u1 t0)).(\lambda (H4: (eq T t0 u2)).(let H5 \def (eq_ind T t0
+(\lambda (t: T).(subst0 i u u1 t)) H3 u2 H4) in (ex2_ind T (\lambda (t:
+T).(subst0 j u1 t1 t)) (\lambda (t: T).(subst0 (S (plus i j)) u t t3)) (ex2 T