-(y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda (x4: T).(\lambda (x5:
-T).(\lambda (H15: (eq T (lift (S O) d x1) (THead (Bind Abst) x4
-x5))).(\lambda (H16: (subst1 d u0 u x4)).(\lambda (H17: (subst1 (s (Bind
-Abst) d) u0 t x5)).(let H18 \def (sym_eq T (lift (S O) d x1) (THead (Bind
-Abst) x4 x5) H15) in (ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T x1
-(THead (Bind Abst) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T x4 (lift (S
-O) d y)))) (\lambda (_: T).(\lambda (z: T).(eq T x5 (lift (S O) (S d) z))))
-(ex3_2 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)))) (\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 Abst) x3 x7))
-(eq_ind_r T (THead (Bind Abst) (lift (S O) d x3) (lift (S O) (S d) x7))
-(\lambda (t0: T).(subst1 (s (Flat Appl) d) u0 (THead (Bind Abst) u t) t0))
-(subst1_head u0 u (lift (S O) d x3) (s (Flat Appl) d) H13 (Bind Abst) t (lift
-(S O) (S d) x7) H22) (lift (S O) d (THead (Bind Abst) x3 x7)) (lift_bind Abst
-x3 x7 (S O) d))) (lift (S O) d (THead (Flat Appl) x2 (THead (Bind Abst) x3
-x7))) (lift_flat Appl x2 (THead (Bind Abst) x3 x7) (S O) d)) (ty3_appl g a x2
-x3 H14 x0 x7 H25))))))))))) (lift_gen_bind Abst x4 x5 x1 (S O) d H18))))))))
-(subst1_gen_head (Bind Abst) u0 u t (lift (S O) d x1) d H9))))))) H11)))))))
-H7))))))))))))))))))) (\lambda (c0: C).(\lambda (t3: T).(\lambda (t4:
-T).(\lambda (_: (ty3 g c0 t3 t4)).(\lambda (H1: ((\forall (e: C).(\forall (u:
-T).(\forall (d: nat).((getl d c0 (CHead e (Bind Abbr) u)) \to (\forall (a0:
-C).((csubst1 d u c0 a0) \to (\forall (a: C).((drop (S O) d a0 a) \to (ex3_2 T
-T (\lambda (y1: T).(\lambda (_: T).(subst1 d u t3 (lift (S O) d y1))))
-(\lambda (_: T).(\lambda (y2: T).(subst1 d u t4 (lift (S O) d y2)))) (\lambda
-(y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))))))))))))).(\lambda (t0:
-T).(\lambda (_: (ty3 g c0 t4 t0)).(\lambda (H3: ((\forall (e: C).(\forall (u:
-T).(\forall (d: nat).((getl d c0 (CHead e (Bind Abbr) u)) \to (\forall (a0:
-C).((csubst1 d u c0 a0) \to (\forall (a: C).((drop (S O) d a0 a) \to (ex3_2 T
-T (\lambda (y1: T).(\lambda (_: T).(subst1 d u t4 (lift (S O) d y1))))
-(\lambda (_: T).(\lambda (y2: T).(subst1 d u t0 (lift (S O) d y2)))) (\lambda
-(y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))))))))))))).(\lambda (e:
-C).(\lambda (u: T).(\lambda (d: nat).(\lambda (H4: (getl d c0 (CHead e (Bind
-Abbr) u))).(\lambda (a0: C).(\lambda (H5: (csubst1 d u c0 a0)).(\lambda (a:
-C).(\lambda (H6: (drop (S O) d a0 a)).(let H7 \def (H3 e u d H4 a0 H5 a H6)
-in (ex3_2_ind T T (\lambda (y1: T).(\lambda (_: T).(subst1 d u t4 (lift (S O)
-d y1)))) (\lambda (_: T).(\lambda (y2: T).(subst1 d u t0 (lift (S O) d y2))))
-(\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2))) (ex3_2 T T (\lambda (y1:
-T).(\lambda (_: T).(subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1))))
-(\lambda (_: T).(\lambda (y2: T).(subst1 d u (THead (Flat Cast) t0 t4) (lift
-(S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda
-(x0: T).(\lambda (x1: T).(\lambda (H8: (subst1 d u t4 (lift (S O) d
-x0))).(\lambda (H9: (subst1 d u t0 (lift (S O) d x1))).(\lambda (H10: (ty3 g
-a x0 x1)).(let H11 \def (H1 e u d H4 a0 H5 a H6) in (ex3_2_ind T T (\lambda
-(y1: T).(\lambda (_: T).(subst1 d u t3 (lift (S O) d y1)))) (\lambda (_:
-T).(\lambda (y2: T).(subst1 d u t4 (lift (S O) d y2)))) (\lambda (y1:
+(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
+Abst) x3 x7)) (eq_ind_r T (THead (Bind Abst) (lift (S O) d x3) (lift (S O) (S
+d) x7)) (\lambda (t0: T).(subst1 (s (Flat Appl) d) u0 (THead (Bind Abst) u t)
+t0)) (subst1_head u0 u (lift (S O) d x3) (s (Flat Appl) d) H13 (Bind Abst) t
+(lift (S O) (S d) x7) H23) (lift (S O) d (THead (Bind Abst) x3 x7))
+(lift_bind Abst x3 x7 (S O) d))) (lift (S O) d (THead (Flat Appl) x2 (THead
+(Bind Abst) x3 x7))) (lift_flat Appl x2 (THead (Bind Abst) x3 x7) (S O) d))
+(ty3_appl g a x2 x3 H14 x0 x7 H26))))))))))) (lift_gen_bind Abst x4 x5 x1 (S
+O) d H19)))))))) H15)))))))) H11))))))) H7))))))))))))))))))) (\lambda (c0:
+C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (ty3 g c0 t3 t4)).(\lambda
+(H1: ((\forall (e: C).(\forall (u: T).(\forall (d: nat).((getl d c0 (CHead e
+(Bind Abbr) u)) \to (\forall (a0: C).((csubst1 d u c0 a0) \to (\forall (a:
+C).((drop (S O) d a0 a) \to (ex3_2 T T (\lambda (y1: T).(\lambda (_:
+T).(subst1 d u t3 (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2:
+T).(subst1 d u t4 (lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3
+g a y1 y2)))))))))))))).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t4
+t0)).(\lambda (H3: ((\forall (e: C).(\forall (u: T).(\forall (d: nat).((getl
+d c0 (CHead e (Bind Abbr) u)) \to (\forall (a0: C).((csubst1 d u c0 a0) \to
+(\forall (a: C).((drop (S O) d a0 a) \to (ex3_2 T T (\lambda (y1: T).(\lambda
+(_: T).(subst1 d u t4 (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2:
+T).(subst1 d u t0 (lift (S O) d y2)))) (\lambda (y1: T).(\lambda (y2: T).(ty3
+g a y1 y2)))))))))))))).(\lambda (e: C).(\lambda (u: T).(\lambda (d:
+nat).(\lambda (H4: (getl d c0 (CHead e (Bind Abbr) u))).(\lambda (a0:
+C).(\lambda (H5: (csubst1 d u c0 a0)).(\lambda (a: C).(\lambda (H6: (drop (S
+O) d a0 a)).(let H7 \def (H3 e u d H4 a0 H5 a H6) in (ex3_2_ind T T (\lambda
+(y1: T).(\lambda (_: T).(subst1 d u t4 (lift (S O) d y1)))) (\lambda (_:
+T).(\lambda (y2: T).(subst1 d u t0 (lift (S O) d y2)))) (\lambda (y1: