-(H: (subst1 i u t0 (lift (S O) i t1))).(let TMP_1 \def (S O) in (let TMP_2
-\def (lift TMP_1 i t1) in (let TMP_3 \def (\lambda (t: T).(subst1 i u t0 t))
-in (let TMP_4 \def (\lambda (_: T).(\forall (t2: T).((subst1 i u t0 (lift (S
-O) i t2)) \to (eq T t1 t2)))) in (let TMP_70 \def (\lambda (y: T).(\lambda
-(H0: (subst1 i u t0 y)).(let TMP_5 \def (\lambda (t: T).((eq T t (lift (S O)
-i t1)) \to (\forall (t2: T).((subst1 i u t0 (lift (S O) i t2)) \to (eq T t1
-t2))))) in (let TMP_32 \def (\lambda (H1: (eq T t0 (lift (S O) i
-t1))).(\lambda (t2: T).(\lambda (H2: (subst1 i u t0 (lift (S O) i t2))).(let
-TMP_8 \def (\lambda (t: T).(let TMP_6 \def (S O) in (let TMP_7 \def (lift
-TMP_6 i t2) in (subst1 i u t TMP_7)))) in (let TMP_9 \def (S O) in (let
-TMP_10 \def (lift TMP_9 i t1) in (let H3 \def (eq_ind T t0 TMP_8 H2 TMP_10
-H1) in (let TMP_11 \def (S O) in (let TMP_12 \def (lift TMP_11 i t2) in (let
-TMP_13 \def (S O) in (let TMP_14 \def (lift TMP_13 i t1) in (let TMP_15 \def
-(S O) in (let TMP_16 \def (lift TMP_15 i t2) in (let TMP_17 \def (S O) in
-(let TMP_18 \def (le_n i) in (let TMP_19 \def (S O) in (let TMP_20 \def (plus
-TMP_19 i) in (let TMP_21 \def (\lambda (n: nat).(lt i n)) in (let TMP_22 \def
-(S O) in (let TMP_23 \def (plus TMP_22 i) in (let TMP_24 \def (le_n TMP_23)
-in (let TMP_25 \def (S O) in (let TMP_26 \def (plus i TMP_25) in (let TMP_27
-\def (S O) in (let TMP_28 \def (plus_sym i TMP_27) in (let TMP_29 \def
-(eq_ind_r nat TMP_20 TMP_21 TMP_24 TMP_26 TMP_28) in (let TMP_30 \def
-(subst1_gen_lift_eq t1 u TMP_16 TMP_17 i i TMP_18 TMP_29 H3) in (let H4 \def
-(sym_eq T TMP_12 TMP_14 TMP_30) in (let TMP_31 \def (S O) in (lift_inj t1 t2
-TMP_31 i H4)))))))))))))))))))))))))))))) in (let TMP_69 \def (\lambda (t2:
-T).(\lambda (H1: (subst0 i u t0 t2)).(\lambda (H2: (eq T t2 (lift (S O) i
-t1))).(\lambda (t3: T).(\lambda (H3: (subst1 i u t0 (lift (S O) i t3))).(let
-TMP_33 \def (\lambda (t: T).(subst0 i u t0 t)) in (let TMP_34 \def (S O) in
-(let TMP_35 \def (lift TMP_34 i t1) in (let H4 \def (eq_ind T t2 TMP_33 H1
-TMP_35 H2) in (let TMP_36 \def (S O) in (let TMP_37 \def (lift TMP_36 i t3)
-in (let TMP_38 \def (\lambda (t: T).(subst1 i u t0 t)) in (let TMP_39 \def
-(\lambda (_: T).(eq T t1 t3)) in (let TMP_68 \def (\lambda (y0: T).(\lambda
-(H5: (subst1 i u t0 y0)).(let TMP_40 \def (\lambda (t: T).((eq T t (lift (S
-O) i t3)) \to (eq T t1 t3))) in (let TMP_62 \def (\lambda (H6: (eq T t0 (lift
-(S O) i t3))).(let TMP_43 \def (\lambda (t: T).(let TMP_41 \def (S O) in (let
-TMP_42 \def (lift TMP_41 i t1) in (subst0 i u t TMP_42)))) in (let TMP_44
-\def (S O) in (let TMP_45 \def (lift TMP_44 i t3) in (let H7 \def (eq_ind T
-t0 TMP_43 H4 TMP_45 H6) in (let TMP_46 \def (S O) in (let TMP_47 \def (lift
-TMP_46 i t1) in (let TMP_48 \def (S O) in (let TMP_49 \def (le_n i) in (let
-TMP_50 \def (S O) in (let TMP_51 \def (plus TMP_50 i) in (let TMP_52 \def
-(\lambda (n: nat).(lt i n)) in (let TMP_53 \def (S O) in (let TMP_54 \def
-(plus TMP_53 i) in (let TMP_55 \def (le_n TMP_54) in (let TMP_56 \def (S O)
-in (let TMP_57 \def (plus i TMP_56) in (let TMP_58 \def (S O) in (let TMP_59
-\def (plus_sym i TMP_58) in (let TMP_60 \def (eq_ind_r nat TMP_51 TMP_52
-TMP_55 TMP_57 TMP_59) in (let TMP_61 \def (eq T t1 t3) in
-(subst0_gen_lift_false t3 u TMP_47 TMP_48 i i TMP_49 TMP_60 H7
-TMP_61)))))))))))))))))))))) in (let TMP_67 \def (\lambda (t4: T).(\lambda
-(H6: (subst0 i u t0 t4)).(\lambda (H7: (eq T t4 (lift (S O) i t3))).(let
-TMP_63 \def (\lambda (t: T).(subst0 i u t0 t)) in (let TMP_64 \def (S O) in
-(let TMP_65 \def (lift TMP_64 i t3) in (let H8 \def (eq_ind T t4 TMP_63 H6
-TMP_65 H7) in (let TMP_66 \def (subst0_confluence_lift t0 t3 u i H8 t1 H4) in
-(sym_eq T t3 t1 TMP_66))))))))) in (subst1_ind i u t0 TMP_40 TMP_62 TMP_67 y0
-H5)))))) in (insert_eq T TMP_37 TMP_38 TMP_39 TMP_68 H3))))))))))))))) in
-(subst1_ind i u t0 TMP_5 TMP_32 TMP_69 y H0)))))) in (insert_eq T TMP_2 TMP_3
-TMP_4 TMP_70 H)))))))))).
+(H: (subst1 i u t0 (lift (S O) i t1))).(insert_eq T (lift (S O) i t1)
+(\lambda (t: T).(subst1 i u t0 t)) (\lambda (_: T).(\forall (t2: T).((subst1
+i u t0 (lift (S O) i t2)) \to (eq T t1 t2)))) (\lambda (y: T).(\lambda (H0:
+(subst1 i u t0 y)).(subst1_ind i u t0 (\lambda (t: T).((eq T t (lift (S O) i
+t1)) \to (\forall (t2: T).((subst1 i u t0 (lift (S O) i t2)) \to (eq T t1
+t2))))) (\lambda (H1: (eq T t0 (lift (S O) i t1))).(\lambda (t2: T).(\lambda
+(H2: (subst1 i u t0 (lift (S O) i t2))).(let H3 \def (eq_ind T t0 (\lambda
+(t: T).(subst1 i u t (lift (S O) i t2))) H2 (lift (S O) i t1) H1) in (let H4
+\def (sym_eq T (lift (S O) i t2) (lift (S O) i t1) (subst1_gen_lift_eq t1 u
+(lift (S O) i t2) (S O) i i (le_n i) (eq_ind_r nat (plus (S O) i) (\lambda
+(n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i (S O)) (plus_sym i (S O)))
+H3)) in (lift_inj t1 t2 (S O) i H4)))))) (\lambda (t2: T).(\lambda (H1:
+(subst0 i u t0 t2)).(\lambda (H2: (eq T t2 (lift (S O) i t1))).(\lambda (t3:
+T).(\lambda (H3: (subst1 i u t0 (lift (S O) i t3))).(let H4 \def (eq_ind T t2
+(\lambda (t: T).(subst0 i u t0 t)) H1 (lift (S O) i t1) H2) in (insert_eq T
+(lift (S O) i t3) (\lambda (t: T).(subst1 i u t0 t)) (\lambda (_: T).(eq T t1
+t3)) (\lambda (y0: T).(\lambda (H5: (subst1 i u t0 y0)).(subst1_ind i u t0
+(\lambda (t: T).((eq T t (lift (S O) i t3)) \to (eq T t1 t3))) (\lambda (H6:
+(eq T t0 (lift (S O) i t3))).(let H7 \def (eq_ind T t0 (\lambda (t:
+T).(subst0 i u t (lift (S O) i t1))) H4 (lift (S O) i t3) H6) in
+(subst0_gen_lift_false t3 u (lift (S O) i t1) (S O) i i (le_n i) (eq_ind_r
+nat (plus (S O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i
+(S O)) (plus_sym i (S O))) H7 (eq T t1 t3)))) (\lambda (t4: T).(\lambda (H6:
+(subst0 i u t0 t4)).(\lambda (H7: (eq T t4 (lift (S O) i t3))).(let H8 \def
+(eq_ind T t4 (\lambda (t: T).(subst0 i u t0 t)) H6 (lift (S O) i t3) H7) in
+(sym_eq T t3 t1 (subst0_confluence_lift t0 t3 u i H8 t1 H4)))))) y0 H5)))
+H3))))))) y H0))) H))))).