-c t0)) (\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat Appl) v (THead
-(Bind Abst) w t))))) (\lambda (y: T).(\lambda (H0: (sn3 c y)).(unintro T t
-(\lambda (t0: T).((eq T y (THead (Bind Abbr) v t0)) \to (\forall (w: T).((sn3
-c w) \to (sn3 c (THead (Flat Appl) v (THead (Bind Abst) w t0))))))) (unintro
-T v (\lambda (t0: T).(\forall (x: T).((eq T y (THead (Bind Abbr) t0 x)) \to
-(\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat Appl) t0 (THead (Bind
-Abst) w x)))))))) (sn3_ind c (\lambda (t0: T).(\forall (x: T).(\forall (x0:
-T).((eq T t0 (THead (Bind Abbr) x x0)) \to (\forall (w: T).((sn3 c w) \to
-(sn3 c (THead (Flat Appl) x (THead (Bind Abst) w x0))))))))) (\lambda (t1:
-T).(\lambda (H1: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P:
-Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2)))))).(\lambda (H2: ((\forall
-(t2: T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to
-(\forall (x: T).(\forall (x0: T).((eq T t2 (THead (Bind Abbr) x x0)) \to
-(\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat Appl) x (THead (Bind Abst)
-w x0))))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H3: (eq T t1
-(THead (Bind Abbr) x x0))).(\lambda (w: T).(\lambda (H4: (sn3 c w)).(let H5
-\def (eq_ind T t1 (\lambda (t0: T).(\forall (t2: T).((((eq T t0 t2) \to
-(\forall (P: Prop).P))) \to ((pr3 c t0 t2) \to (\forall (x1: T).(\forall (x2:
-T).((eq T t2 (THead (Bind Abbr) x1 x2)) \to (\forall (w0: T).((sn3 c w0) \to
-(sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) w0 x2)))))))))))) H2 (THead
-(Bind Abbr) x x0) H3) in (let H6 \def (eq_ind T t1 (\lambda (t0: T).(\forall
-(t2: T).((((eq T t0 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t2) \to
-(sn3 c t2))))) H1 (THead (Bind Abbr) x x0) H3) in (sn3_ind c (\lambda (t0:
-T).(sn3 c (THead (Flat Appl) x (THead (Bind Abst) t0 x0)))) (\lambda (t2:
-T).(\lambda (H7: ((\forall (t3: T).((((eq T t2 t3) \to (\forall (P:
-Prop).P))) \to ((pr3 c t2 t3) \to (sn3 c t3)))))).(\lambda (H8: ((\forall
-(t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to
-(sn3 c (THead (Flat Appl) x (THead (Bind Abst) t3 x0)))))))).(sn3_pr2_intro c
-(THead (Flat Appl) x (THead (Bind Abst) t2 x0)) (\lambda (t3: T).(\lambda
-(H9: (((eq T (THead (Flat Appl) x (THead (Bind Abst) t2 x0)) t3) \to (\forall
-(P: Prop).P)))).(\lambda (H10: (pr2 c (THead (Flat Appl) x (THead (Bind Abst)
-t2 x0)) t3)).(let H11 \def (pr2_gen_appl c x (THead (Bind Abst) t2 x0) t3
-H10) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead
-(Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
-(\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Bind Abst) t2 x0) t4))))
-(ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
-T).(eq T (THead (Bind Abst) t2 x0) (THead (Bind Abst) y1 z1)))))) (\lambda
-(_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead
-(Bind Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
-T).(\lambda (_: T).(pr2 c x u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda
-(_: T).(\lambda (t4: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind
-b) u) z1 t4)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_:
-T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
-b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
-T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind Abst) t2 x0) (THead
-(Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
-T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t3 (THead (Bind
-b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
-B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
-(_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
-T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
-(\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
-(_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))) (sn3 c t3)
-(\lambda (H12: (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead
-(Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
-(\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Bind Abst) t2 x0)
-t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead
-(Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
-(\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Bind Abst) t2 x0) t4))) (sn3
-c t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (H13: (eq T t3 (THead (Flat
-Appl) x1 x2))).(\lambda (H14: (pr2 c x x1)).(\lambda (H15: (pr2 c (THead
-(Bind Abst) t2 x0) x2)).(let H16 \def (eq_ind T t3 (\lambda (t0: T).((eq T
-(THead (Flat Appl) x (THead (Bind Abst) t2 x0)) t0) \to (\forall (P:
-Prop).P))) H9 (THead (Flat Appl) x1 x2) H13) in (eq_ind_r T (THead (Flat
-Appl) x1 x2) (\lambda (t0: T).(sn3 c t0)) (let H17 \def (pr2_gen_abst c t2 x0
-x2 H15) in (ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead
-(Bind Abst) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c t2 u2)))
-(\lambda (_: T).(\lambda (t4: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead
-c (Bind b) u) x0 t4))))) (sn3 c (THead (Flat Appl) x1 x2)) (\lambda (x3:
-T).(\lambda (x4: T).(\lambda (H18: (eq T x2 (THead (Bind Abst) x3
-x4))).(\lambda (H19: (pr2 c t2 x3)).(\lambda (H20: ((\forall (b: B).(\forall
-(u: T).(pr2 (CHead c (Bind b) u) x0 x4))))).(let H21 \def (eq_ind T x2
-(\lambda (t0: T).((eq T (THead (Flat Appl) x (THead (Bind Abst) t2 x0))
+c t0)) (\lambda (_: T).(\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat
+Appl) v (THead (Bind Abst) w t)))))) (\lambda (y: T).(\lambda (H0: (sn3 c
+y)).(unintro T t (\lambda (t0: T).((eq T y (THead (Bind Abbr) v t0)) \to
+(\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat Appl) v (THead (Bind Abst)
+w t0))))))) (unintro T v (\lambda (t0: T).(\forall (x: T).((eq T y (THead
+(Bind Abbr) t0 x)) \to (\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat
+Appl) t0 (THead (Bind Abst) w x)))))))) (sn3_ind c (\lambda (t0: T).(\forall
+(x: T).(\forall (x0: T).((eq T t0 (THead (Bind Abbr) x x0)) \to (\forall (w:
+T).((sn3 c w) \to (sn3 c (THead (Flat Appl) x (THead (Bind Abst) w
+x0))))))))) (\lambda (t1: T).(\lambda (H1: ((\forall (t2: T).((((eq T t1 t2)
+\to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2)))))).(\lambda
+(H2: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3
+c t1 t2) \to (\forall (x: T).(\forall (x0: T).((eq T t2 (THead (Bind Abbr) x
+x0)) \to (\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat Appl) x (THead
+(Bind Abst) w x0))))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H3:
+(eq T t1 (THead (Bind Abbr) x x0))).(\lambda (w: T).(\lambda (H4: (sn3 c
+w)).(let H5 \def (eq_ind T t1 (\lambda (t0: T).(\forall (t2: T).((((eq T t0
+t2) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t2) \to (\forall (x1:
+T).(\forall (x2: T).((eq T t2 (THead (Bind Abbr) x1 x2)) \to (\forall (w0:
+T).((sn3 c w0) \to (sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) w0
+x2)))))))))))) H2 (THead (Bind Abbr) x x0) H3) in (let H6 \def (eq_ind T t1
+(\lambda (t0: T).(\forall (t2: T).((((eq T t0 t2) \to (\forall (P: Prop).P)))
+\to ((pr3 c t0 t2) \to (sn3 c t2))))) H1 (THead (Bind Abbr) x x0) H3) in
+(sn3_ind c (\lambda (t0: T).(sn3 c (THead (Flat Appl) x (THead (Bind Abst) t0
+x0)))) (\lambda (t2: T).(\lambda (H7: ((\forall (t3: T).((((eq T t2 t3) \to
+(\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to (sn3 c t3)))))).(\lambda (H8:
+((\forall (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t2
+t3) \to (sn3 c (THead (Flat Appl) x (THead (Bind Abst) t3
+x0)))))))).(sn3_pr2_intro c (THead (Flat Appl) x (THead (Bind Abst) t2 x0))
+(\lambda (t3: T).(\lambda (H9: (((eq T (THead (Flat Appl) x (THead (Bind
+Abst) t2 x0)) t3) \to (\forall (P: Prop).P)))).(\lambda (H10: (pr2 c (THead
+(Flat Appl) x (THead (Bind Abst) t2 x0)) t3)).(let H11 \def (pr2_gen_appl c x
+(THead (Bind Abst) t2 x0) t3 H10) in (or3_ind (ex3_2 T T (\lambda (u2:
+T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2:
+T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c
+(THead (Bind Abst) t2 x0) t4)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
+(z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind Abst) t2 x0)
+(THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
+T).(\lambda (t4: T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
+(_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b:
+B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4)))))))) (ex6_6 B T T T T T
+(\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
+T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T
+(THead (Bind Abst) t2 x0) (THead (Bind b) y1 z1)))))))) (\lambda (b:
+B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
+(y2: T).(eq T t3 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2)
+z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
+T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_:
+B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
+(y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
+T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b)
+y2) z1 z2)))))))) (sn3 c t3) (\lambda (H12: (ex3_2 T T (\lambda (u2:
+T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2:
+T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c
+(THead (Bind Abst) t2 x0) t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda
+(t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_:
+T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Bind Abst)
+t2 x0) t4))) (sn3 c t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (H13: (eq
+T t3 (THead (Flat Appl) x1 x2))).(\lambda (H14: (pr2 c x x1)).(\lambda (H15:
+(pr2 c (THead (Bind Abst) t2 x0) x2)).(let H16 \def (eq_ind T t3 (\lambda
+(t0: T).((eq T (THead (Flat Appl) x (THead (Bind Abst) t2 x0)) t0) \to
+(\forall (P: Prop).P))) H9 (THead (Flat Appl) x1 x2) H13) in (eq_ind_r T
+(THead (Flat Appl) x1 x2) (\lambda (t0: T).(sn3 c t0)) (let H17 \def
+(pr2_gen_abst c t2 x0 x2 H15) in (ex3_2_ind T T (\lambda (u2: T).(\lambda
+(t4: T).(eq T x2 (THead (Bind Abst) u2 t4)))) (\lambda (u2: T).(\lambda (_:
+T).(pr2 c t2 u2))) (\lambda (_: T).(\lambda (t4: T).(\forall (b: B).(\forall
+(u: T).(pr2 (CHead c (Bind b) u) x0 t4))))) (sn3 c (THead (Flat Appl) x1 x2))
+(\lambda (x3: T).(\lambda (x4: T).(\lambda (H18: (eq T x2 (THead (Bind Abst)
+x3 x4))).(\lambda (H19: (pr2 c t2 x3)).(\lambda (H20: ((\forall (b:
+B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x0 x4))))).(let H21 \def (eq_ind
+T x2 (\lambda (t0: T).((eq T (THead (Flat Appl) x (THead (Bind Abst) t2 x0))