-(\lambda (x6: T).(\lambda (x7: T).(\lambda (H19: (eq T x1 (THead (Bind Abst)
-x6 x7))).(\lambda (H20: (eq T x4 (lift (S O) d x6))).(\lambda (H21: (eq T x5
-(lift (S O) (S d) x7))).(let H22 \def (eq_ind T x5 (\lambda (t0: T).(subst1
-(s (Bind Abst) d) u0 t t0)) H17 (lift (S O) (S d) x7) H21) in (let H23 \def
-(eq_ind T x4 (\lambda (t0: T).(subst1 d u0 u t0)) H16 (lift (S O) d x6) H20)
-in (let H24 \def (eq_ind T x1 (\lambda (t0: T).(ty3 g a x0 t0)) H10 (THead
-(Bind Abst) x6 x7) H19) in (let H25 \def (eq_ind T x6 (\lambda (t0: T).(ty3 g
-a x0 (THead (Bind Abst) t0 x7))) H24 x3 (subst1_confluence_lift u x6 u0 d H23
-x3 H13)) in (ex3_2_intro T T (\lambda (y1: T).(\lambda (_: T).(subst1 d u0
-(THead (Flat Appl) w v) (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2:
-T).(subst1 d u0 (THead (Flat Appl) w (THead (Bind Abst) u t)) (lift (S O) d
-y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))) (THead (Flat Appl)
-x2 x0) (THead (Flat Appl) x2 (THead (Bind Abst) x3 x7)) (eq_ind_r T (THead
-(Flat Appl) (lift (S O) d x2) (lift (S O) d x0)) (\lambda (t0: T).(subst1 d
-u0 (THead (Flat Appl) w v) t0)) (subst1_head u0 w (lift (S O) d x2) d H12
-(Flat Appl) v (lift (S O) d x0) H8) (lift (S O) d (THead (Flat Appl) x2 x0))
-(lift_flat Appl x2 x0 (S O) d)) (eq_ind_r T (THead (Flat Appl) (lift (S O) d
-x2) (lift (S O) d (THead (Bind Abst) x3 x7))) (\lambda (t0: T).(subst1 d u0
-(THead (Flat Appl) w (THead (Bind Abst) u t)) t0)) (subst1_head u0 w (lift (S
-O) d x2) d H12 (Flat Appl) (THead (Bind Abst) u t) (lift (S O) d (THead (Bind
+(\lambda (x6: T).(\lambda (x7: T).(\lambda (H20: (eq T x1 (THead (Bind Abst)
+x6 x7))).(\lambda (H21: (eq T x4 (lift (S O) d x6))).(\lambda (H22: (eq T x5
+(lift (S O) (S d) x7))).(let H23 \def (eq_ind T x5 (\lambda (t0: T).(subst1
+(S d) u0 t t0)) H18 (lift (S O) (S d) x7) H22) in (let H24 \def (eq_ind T x4
+(\lambda (t0: T).(subst1 d u0 u t0)) H17 (lift (S O) d x6) H21) in (let H25
+\def (eq_ind T x1 (\lambda (t0: T).(ty3 g a x0 t0)) H10 (THead (Bind Abst) x6
+x7) H20) in (let H26 \def (eq_ind T x6 (\lambda (t0: T).(ty3 g a x0 (THead
+(Bind Abst) t0 x7))) H25 x3 (subst1_confluence_lift u x6 u0 d H24 x3 H13)) in
+(ex3_2_intro T T (\lambda (y1: T).(\lambda (_: T).(subst1 d u0 (THead (Flat
+Appl) w v) (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(subst1 d u0
+(THead (Flat Appl) w (THead (Bind Abst) u t)) (lift (S O) d y2)))) (\lambda
+(y1: T).(\lambda (y2: T).(ty3 g a y1 y2))) (THead (Flat Appl) x2 x0) (THead
+(Flat Appl) x2 (THead (Bind Abst) x3 x7)) (eq_ind_r T (THead (Flat Appl)
+(lift (S O) d x2) (lift (S O) d x0)) (\lambda (t0: T).(subst1 d u0 (THead
+(Flat Appl) w v) t0)) (subst1_head u0 w (lift (S O) d x2) d H12 (Flat Appl) v
+(lift (S O) d x0) H8) (lift (S O) d (THead (Flat Appl) x2 x0)) (lift_flat
+Appl x2 x0 (S O) d)) (eq_ind_r T (THead (Flat Appl) (lift (S O) d x2) (lift
+(S O) d (THead (Bind Abst) x3 x7))) (\lambda (t0: T).(subst1 d u0 (THead
+(Flat Appl) w (THead (Bind Abst) u t)) t0)) (subst1_head u0 w (lift (S O) d
+x2) d H12 (Flat Appl) (THead (Bind Abst) u t) (lift (S O) d (THead (Bind