(* This file was automatically generated: do not edit *********************)
-
+set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/props".
include "sn3/nf2.ma".
\def
\lambda (c: C).(\lambda (v: T).(\lambda (t: T).(\lambda (H: (sn3 c (THead
(Bind Abbr) v t))).(insert_eq T (THead (Bind Abbr) v t) (\lambda (t0: T).(sn3
-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))
(THead (Flat Appl) x1 t0)) \to (\forall (P: Prop).P))) H16 (THead (Bind Abst)
x3 x4) H18) in (eq_ind_r T (THead (Bind Abst) x3 x4) (\lambda (t0: T).(sn3 c
(THead (Flat Appl) x1 t0))) (let H_x \def (term_dec t2 x3) in (let H22 \def
\lambda (c: C).(\lambda (d: C).(\lambda (w: T).(\lambda (i: nat).(\lambda
(H: (getl i c (CHead d (Bind Abbr) w))).(\lambda (v: T).(\lambda (H0: (sn3 c
(THead (Flat Appl) v (lift (S i) O w)))).(insert_eq T (THead (Flat Appl) v
-(lift (S i) O w)) (\lambda (t: T).(sn3 c t)) (sn3 c (THead (Flat Appl) v
-(TLRef i))) (\lambda (y: T).(\lambda (H1: (sn3 c y)).(unintro T v (\lambda
-(t: T).((eq T y (THead (Flat Appl) t (lift (S i) O w))) \to (sn3 c (THead
-(Flat Appl) t (TLRef i))))) (sn3_ind c (\lambda (t: T).(\forall (x: T).((eq T
-t (THead (Flat Appl) x (lift (S i) O w))) \to (sn3 c (THead (Flat Appl) x
-(TLRef i)))))) (\lambda (t1: T).(\lambda (H2: ((\forall (t2: T).((((eq T t1
-t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c
+(lift (S i) O w)) (\lambda (t: T).(sn3 c t)) (\lambda (_: T).(sn3 c (THead
+(Flat Appl) v (TLRef i)))) (\lambda (y: T).(\lambda (H1: (sn3 c y)).(unintro
+T v (\lambda (t: T).((eq T y (THead (Flat Appl) t (lift (S i) O w))) \to (sn3
+c (THead (Flat Appl) t (TLRef i))))) (sn3_ind c (\lambda (t: T).(\forall (x:
+T).((eq T t (THead (Flat Appl) x (lift (S i) O w))) \to (sn3 c (THead (Flat
+Appl) x (TLRef i)))))) (\lambda (t1: T).(\lambda (H2: ((\forall (t2:
+T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c
t2)))))).(\lambda (H3: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P:
Prop).P))) \to ((pr3 c t1 t2) \to (\forall (x: T).((eq T t2 (THead (Flat
Appl) x (lift (S i) O w))) \to (sn3 c (THead (Flat Appl) x (TLRef
\def
\lambda (c: C).(\lambda (v: T).(\lambda (u: T).(\lambda (H: (sn3 c (THead
(Flat Appl) v u))).(insert_eq T (THead (Flat Appl) v u) (\lambda (t: T).(sn3
-c t)) (\forall (t: T).((sn3 c (THead (Flat Appl) v t)) \to (sn3 c (THead
-(Flat Appl) v (THead (Flat Cast) u t))))) (\lambda (y: T).(\lambda (H0: (sn3
-c y)).(unintro T u (\lambda (t: T).((eq T y (THead (Flat Appl) v t)) \to
-(\forall (t0: T).((sn3 c (THead (Flat Appl) v t0)) \to (sn3 c (THead (Flat
-Appl) v (THead (Flat Cast) t t0))))))) (unintro T v (\lambda (t: T).(\forall
-(x: T).((eq T y (THead (Flat Appl) t x)) \to (\forall (t0: T).((sn3 c (THead
-(Flat Appl) t t0)) \to (sn3 c (THead (Flat Appl) t (THead (Flat Cast) x
-t0)))))))) (sn3_ind c (\lambda (t: T).(\forall (x: T).(\forall (x0: T).((eq T
-t (THead (Flat Appl) x x0)) \to (\forall (t0: T).((sn3 c (THead (Flat Appl) x
-t0)) \to (sn3 c (THead (Flat Appl) x (THead (Flat Cast) x0 t0)))))))))
-(\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 (Flat Appl) x x0)) \to
-(\forall (t: T).((sn3 c (THead (Flat Appl) x t)) \to (sn3 c (THead (Flat
-Appl) x (THead (Flat Cast) x0 t))))))))))))).(\lambda (x: T).(\lambda (x0:
-T).(\lambda (H3: (eq T t1 (THead (Flat Appl) x x0))).(\lambda (t: T).(\lambda
-(H4: (sn3 c (THead (Flat Appl) x t))).(insert_eq T (THead (Flat Appl) x t)
-(\lambda (t0: T).(sn3 c t0)) (sn3 c (THead (Flat Appl) x (THead (Flat Cast)
-x0 t))) (\lambda (y0: T).(\lambda (H5: (sn3 c y0)).(unintro T t (\lambda (t0:
-T).((eq T y0 (THead (Flat Appl) x t0)) \to (sn3 c (THead (Flat Appl) x (THead
-(Flat Cast) x0 t0))))) (sn3_ind c (\lambda (t0: T).(\forall (x1: T).((eq T t0
+c t)) (\lambda (_: T).(\forall (t0: T).((sn3 c (THead (Flat Appl) v t0)) \to
+(sn3 c (THead (Flat Appl) v (THead (Flat Cast) u t0)))))) (\lambda (y:
+T).(\lambda (H0: (sn3 c y)).(unintro T u (\lambda (t: T).((eq T y (THead
+(Flat Appl) v t)) \to (\forall (t0: T).((sn3 c (THead (Flat Appl) v t0)) \to
+(sn3 c (THead (Flat Appl) v (THead (Flat Cast) t t0))))))) (unintro T v
+(\lambda (t: T).(\forall (x: T).((eq T y (THead (Flat Appl) t x)) \to
+(\forall (t0: T).((sn3 c (THead (Flat Appl) t t0)) \to (sn3 c (THead (Flat
+Appl) t (THead (Flat Cast) x t0)))))))) (sn3_ind c (\lambda (t: T).(\forall
+(x: T).(\forall (x0: T).((eq T t (THead (Flat Appl) x x0)) \to (\forall (t0:
+T).((sn3 c (THead (Flat Appl) x t0)) \to (sn3 c (THead (Flat Appl) x (THead
+(Flat Cast) x0 t0))))))))) (\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 (Flat Appl) x x0)) \to (\forall (t: T).((sn3 c (THead (Flat Appl) x
+t)) \to (sn3 c (THead (Flat Appl) x (THead (Flat Cast) x0
+t))))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H3: (eq T t1 (THead
+(Flat Appl) x x0))).(\lambda (t: T).(\lambda (H4: (sn3 c (THead (Flat Appl) x
+t))).(insert_eq T (THead (Flat Appl) x t) (\lambda (t0: T).(sn3 c t0))
+(\lambda (_: T).(sn3 c (THead (Flat Appl) x (THead (Flat Cast) x0 t))))
+(\lambda (y0: T).(\lambda (H5: (sn3 c y0)).(unintro T t (\lambda (t0: T).((eq
+T y0 (THead (Flat Appl) x t0)) \to (sn3 c (THead (Flat Appl) x (THead (Flat
+Cast) x0 t0))))) (sn3_ind c (\lambda (t0: T).(\forall (x1: T).((eq T t0
(THead (Flat Appl) x x1)) \to (sn3 c (THead (Flat Appl) x (THead (Flat Cast)
x0 x1)))))) (\lambda (t0: T).(\lambda (H6: ((\forall (t2: T).((((eq T t0 t2)
\to (\forall (P: Prop).P))) \to ((pr3 c t0 t2) \to (sn3 c t2)))))).(\lambda
t))))))))))).(\lambda (t: T).(\lambda (v: T).(\lambda (H3: (sn3 (CHead c
(Bind b) t1) (THead (Flat Appl) (lift (S O) O v) t))).(insert_eq T (THead
(Flat Appl) (lift (S O) O v) t) (\lambda (t0: T).(sn3 (CHead c (Bind b) t1)
-t0)) (sn3 c (THead (Flat Appl) v (THead (Bind b) t1 t))) (\lambda (y:
-T).(\lambda (H4: (sn3 (CHead c (Bind b) t1) y)).(unintro T t (\lambda (t0:
-T).((eq T y (THead (Flat Appl) (lift (S O) O v) t0)) \to (sn3 c (THead (Flat
-Appl) v (THead (Bind b) t1 t0))))) (unintro T v (\lambda (t0: T).(\forall (x:
-T).((eq T y (THead (Flat Appl) (lift (S O) O t0) x)) \to (sn3 c (THead (Flat
-Appl) t0 (THead (Bind b) t1 x)))))) (sn3_ind (CHead c (Bind b) t1) (\lambda
-(t0: T).(\forall (x: T).(\forall (x0: T).((eq T t0 (THead (Flat Appl) (lift
-(S O) O x) x0)) \to (sn3 c (THead (Flat Appl) x (THead (Bind b) t1 x0)))))))
-(\lambda (t2: T).(\lambda (H5: ((\forall (t3: T).((((eq T t2 t3) \to (\forall
-(P: Prop).P))) \to ((pr3 (CHead c (Bind b) t1) t2 t3) \to (sn3 (CHead c (Bind
-b) t1) t3)))))).(\lambda (H6: ((\forall (t3: T).((((eq T t2 t3) \to (\forall
-(P: Prop).P))) \to ((pr3 (CHead c (Bind b) t1) t2 t3) \to (\forall (x:
-T).(\forall (x0: T).((eq T t3 (THead (Flat Appl) (lift (S O) O x) x0)) \to
-(sn3 c (THead (Flat Appl) x (THead (Bind b) t1 x0))))))))))).(\lambda (x:
-T).(\lambda (x0: T).(\lambda (H7: (eq T t2 (THead (Flat Appl) (lift (S O) O
-x) x0))).(let H8 \def (eq_ind T t2 (\lambda (t0: T).(\forall (t3: T).((((eq T
+t0)) (\lambda (_: T).(sn3 c (THead (Flat Appl) v (THead (Bind b) t1 t))))
+(\lambda (y: T).(\lambda (H4: (sn3 (CHead c (Bind b) t1) y)).(unintro T t
+(\lambda (t0: T).((eq T y (THead (Flat Appl) (lift (S O) O v) t0)) \to (sn3 c
+(THead (Flat Appl) v (THead (Bind b) t1 t0))))) (unintro T v (\lambda (t0:
+T).(\forall (x: T).((eq T y (THead (Flat Appl) (lift (S O) O t0) x)) \to (sn3
+c (THead (Flat Appl) t0 (THead (Bind b) t1 x)))))) (sn3_ind (CHead c (Bind b)
+t1) (\lambda (t0: T).(\forall (x: T).(\forall (x0: T).((eq T t0 (THead (Flat
+Appl) (lift (S O) O x) x0)) \to (sn3 c (THead (Flat Appl) x (THead (Bind b)
+t1 x0))))))) (\lambda (t2: T).(\lambda (H5: ((\forall (t3: T).((((eq T t2 t3)
+\to (\forall (P: Prop).P))) \to ((pr3 (CHead c (Bind b) t1) t2 t3) \to (sn3
+(CHead c (Bind b) t1) t3)))))).(\lambda (H6: ((\forall (t3: T).((((eq T t2
+t3) \to (\forall (P: Prop).P))) \to ((pr3 (CHead c (Bind b) t1) t2 t3) \to
+(\forall (x: T).(\forall (x0: T).((eq T t3 (THead (Flat Appl) (lift (S O) O
+x) x0)) \to (sn3 c (THead (Flat Appl) x (THead (Bind b) t1
+x0))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H7: (eq T t2 (THead
+(Flat Appl) (lift (S O) O x) x0))).(let H8 \def (eq_ind T t2 (\lambda (t0:
+T).(\forall (t3: T).((((eq T t0 t3) \to (\forall (P: Prop).P))) \to ((pr3
+(CHead c (Bind b) t1) t0 t3) \to (\forall (x1: T).(\forall (x2: T).((eq T t3
+(THead (Flat Appl) (lift (S O) O x1) x2)) \to (sn3 c (THead (Flat Appl) x1
+(THead (Bind b) t1 x2)))))))))) H6 (THead (Flat Appl) (lift (S O) O x) x0)
+H7) in (let H9 \def (eq_ind T t2 (\lambda (t0: T).(\forall (t3: T).((((eq T
t0 t3) \to (\forall (P: Prop).P))) \to ((pr3 (CHead c (Bind b) t1) t0 t3) \to
-(\forall (x1: T).(\forall (x2: T).((eq T t3 (THead (Flat Appl) (lift (S O) O
-x1) x2)) \to (sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x2)))))))))) H6
-(THead (Flat Appl) (lift (S O) O x) x0) H7) in (let H9 \def (eq_ind T t2
-(\lambda (t0: T).(\forall (t3: T).((((eq T t0 t3) \to (\forall (P: Prop).P)))
-\to ((pr3 (CHead c (Bind b) t1) t0 t3) \to (sn3 (CHead c (Bind b) t1) t3)))))
-H5 (THead (Flat Appl) (lift (S O) O x) x0) H7) in (sn3_pr2_intro c (THead
-(Flat Appl) x (THead (Bind b) t1 x0)) (\lambda (t3: T).(\lambda (H10: (((eq T
-(THead (Flat Appl) x (THead (Bind b) t1 x0)) t3) \to (\forall (P:
-Prop).P)))).(\lambda (H11: (pr2 c (THead (Flat Appl) x (THead (Bind b) t1
-x0)) t3)).(let H12 \def (pr2_gen_appl c x (THead (Bind b) t1 x0) t3 H11) 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 b) t1 x0) t4)))) (ex4_4 T T T T
-(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
-(THead (Bind b) t1 x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
+(sn3 (CHead c (Bind b) t1) t3))))) H5 (THead (Flat Appl) (lift (S O) O x) x0)
+H7) in (sn3_pr2_intro c (THead (Flat Appl) x (THead (Bind b) t1 x0)) (\lambda
+(t3: T).(\lambda (H10: (((eq T (THead (Flat Appl) x (THead (Bind b) t1 x0))
+t3) \to (\forall (P: Prop).P)))).(\lambda (H11: (pr2 c (THead (Flat Appl) x
+(THead (Bind b) t1 x0)) t3)).(let H12 \def (pr2_gen_appl c x (THead (Bind b)
+t1 x0) t3 H11) 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 b) t1 x0) t4))))
+(ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
+T).(eq T (THead (Bind b) t1 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 (_:
\def
\lambda (v1: T).(\lambda (t1: T).(let u1 \def (THead (Flat Appl) v1 t1) in
(\lambda (c: C).(\lambda (H: (sn3 c (THead (Flat Appl) v1 t1))).(insert_eq T
-(THead (Flat Appl) v1 t1) (\lambda (t: T).(sn3 c t)) (\forall (v2: T).((sn3 c
-v2) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) v1 t1) u2) \to ((((iso
-(THead (Flat Appl) v1 t1) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
-(Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2 (THead (Flat Appl)
-v1 t1)))))) (\lambda (y: T).(\lambda (H0: (sn3 c y)).(unintro T t1 (\lambda
-(t: T).((eq T y (THead (Flat Appl) v1 t)) \to (\forall (v2: T).((sn3 c v2)
-\to (((\forall (u2: T).((pr3 c (THead (Flat Appl) v1 t) u2) \to ((((iso
-(THead (Flat Appl) v1 t) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
-(Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2 (THead (Flat Appl)
-v1 t)))))))) (unintro T v1 (\lambda (t: T).(\forall (x: T).((eq T y (THead
-(Flat Appl) t x)) \to (\forall (v2: T).((sn3 c v2) \to (((\forall (u2:
-T).((pr3 c (THead (Flat Appl) t x) u2) \to ((((iso (THead (Flat Appl) t x)
-u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to
-(sn3 c (THead (Flat Appl) v2 (THead (Flat Appl) t x))))))))) (sn3_ind c
-(\lambda (t: T).(\forall (x: T).(\forall (x0: T).((eq T t (THead (Flat Appl)
-x x0)) \to (\forall (v2: T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c (THead
-(Flat Appl) x x0) u2) \to ((((iso (THead (Flat Appl) x x0) u2) \to (\forall
-(P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c (THead
-(Flat Appl) v2 (THead (Flat Appl) x x0)))))))))) (\lambda (t2: T).(\lambda
-(H1: ((\forall (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P))) \to ((pr3
-c t2 t3) \to (sn3 c t3)))))).(\lambda (H2: ((\forall (t3: T).((((eq T t2 t3)
-\to (\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to (\forall (x: T).(\forall
-(x0: T).((eq T t3 (THead (Flat Appl) x x0)) \to (\forall (v2: T).((sn3 c v2)
-\to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x x0) u2) \to ((((iso
-(THead (Flat Appl) x x0) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
-(Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2 (THead (Flat Appl) x
-x0)))))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H3: (eq T t2
+(THead (Flat Appl) v1 t1) (\lambda (t: T).(sn3 c t)) (\lambda (t: T).(\forall
+(v2: T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c t u2) \to ((((iso t u2)
+\to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to
+(sn3 c (THead (Flat Appl) v2 t)))))) (\lambda (y: T).(\lambda (H0: (sn3 c
+y)).(unintro T t1 (\lambda (t: T).((eq T y (THead (Flat Appl) v1 t)) \to
+(\forall (v2: T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c y u2) \to ((((iso
+y u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2))))))
+\to (sn3 c (THead (Flat Appl) v2 y))))))) (unintro T v1 (\lambda (t:
+T).(\forall (x: T).((eq T y (THead (Flat Appl) t x)) \to (\forall (v2:
+T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c y u2) \to ((((iso y u2) \to
+(\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c
+(THead (Flat Appl) v2 y)))))))) (sn3_ind c (\lambda (t: T).(\forall (x:
+T).(\forall (x0: T).((eq T t (THead (Flat Appl) x x0)) \to (\forall (v2:
+T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c t u2) \to ((((iso t u2) \to
+(\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c
+(THead (Flat Appl) v2 t))))))))) (\lambda (t2: T).(\lambda (H1: ((\forall
+(t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to
+(sn3 c t3)))))).(\lambda (H2: ((\forall (t3: T).((((eq T t2 t3) \to (\forall
+(P: Prop).P))) \to ((pr3 c t2 t3) \to (\forall (x: T).(\forall (x0: T).((eq T
+t3 (THead (Flat Appl) x x0)) \to (\forall (v2: T).((sn3 c v2) \to (((\forall
+(u2: T).((pr3 c t3 u2) \to ((((iso t3 u2) \to (\forall (P: Prop).P))) \to
+(sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2
+t3))))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H3: (eq T t2
(THead (Flat Appl) x x0))).(\lambda (v2: T).(\lambda (H4: (sn3 c
-v2)).(sn3_ind c (\lambda (t: T).(((\forall (u2: T).((pr3 c (THead (Flat Appl)
-x x0) u2) \to ((((iso (THead (Flat Appl) x x0) u2) \to (\forall (P:
-Prop).P))) \to (sn3 c (THead (Flat Appl) t u2)))))) \to (sn3 c (THead (Flat
-Appl) t (THead (Flat Appl) x x0))))) (\lambda (t0: T).(\lambda (H5: ((\forall
+v2)).(sn3_ind c (\lambda (t: T).(((\forall (u2: T).((pr3 c t2 u2) \to ((((iso
+t2 u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t u2))))))
+\to (sn3 c (THead (Flat Appl) t t2)))) (\lambda (t0: T).(\lambda (H5:
+((\forall (t3: T).((((eq T t0 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t0
+t3) \to (sn3 c t3)))))).(\lambda (H6: ((\forall (t3: T).((((eq T t0 t3) \to
+(\forall (P: Prop).P))) \to ((pr3 c t0 t3) \to (((\forall (u2: T).((pr3 c t2
+u2) \to ((((iso t2 u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat
+Appl) t3 u2)))))) \to (sn3 c (THead (Flat Appl) t3 t2)))))))).(\lambda (H7:
+((\forall (u2: T).((pr3 c t2 u2) \to ((((iso t2 u2) \to (\forall (P:
+Prop).P))) \to (sn3 c (THead (Flat Appl) t0 u2))))))).(let H8 \def (eq_ind T
+t2 (\lambda (t: T).(\forall (u2: T).((pr3 c t u2) \to ((((iso t u2) \to
+(\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t0 u2)))))) H7 (THead
+(Flat Appl) x x0) H3) in (let H9 \def (eq_ind T t2 (\lambda (t: T).(\forall
(t3: T).((((eq T t0 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t3) \to
-(sn3 c t3)))))).(\lambda (H6: ((\forall (t3: T).((((eq T t0 t3) \to (\forall
-(P: Prop).P))) \to ((pr3 c t0 t3) \to (((\forall (u2: T).((pr3 c (THead (Flat
-Appl) x x0) u2) \to ((((iso (THead (Flat Appl) x x0) u2) \to (\forall (P:
+(((\forall (u2: T).((pr3 c t u2) \to ((((iso t u2) \to (\forall (P:
Prop).P))) \to (sn3 c (THead (Flat Appl) t3 u2)))))) \to (sn3 c (THead (Flat
-Appl) t3 (THead (Flat Appl) x x0))))))))).(\lambda (H7: ((\forall (u2:
-T).((pr3 c (THead (Flat Appl) x x0) u2) \to ((((iso (THead (Flat Appl) x x0)
-u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t0
-u2))))))).(let H8 \def (eq_ind T t2 (\lambda (t: T).(\forall (t3: T).((((eq T
-t t3) \to (\forall (P: Prop).P))) \to ((pr3 c t t3) \to (\forall (x1:
-T).(\forall (x2: T).((eq T t3 (THead (Flat Appl) x1 x2)) \to (\forall (v3:
-T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x1 x2) u2)
-\to ((((iso (THead (Flat Appl) x1 x2) u2) \to (\forall (P: Prop).P))) \to
-(sn3 c (THead (Flat Appl) v3 u2)))))) \to (sn3 c (THead (Flat Appl) v3 (THead
-(Flat Appl) x1 x2))))))))))))) H2 (THead (Flat Appl) x x0) H3) in (let H9
-\def (eq_ind T t2 (\lambda (t: T).(\forall (t3: T).((((eq T t t3) \to
-(\forall (P: Prop).P))) \to ((pr3 c t t3) \to (sn3 c t3))))) H1 (THead (Flat
-Appl) x x0) H3) in (sn3_pr2_intro c (THead (Flat Appl) t0 (THead (Flat Appl)
-x x0)) (\lambda (t3: T).(\lambda (H10: (((eq T (THead (Flat Appl) t0 (THead
-(Flat Appl) x x0)) t3) \to (\forall (P: Prop).P)))).(\lambda (H11: (pr2 c
-(THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t3)).(let H12 \def
-(pr2_gen_appl c t0 (THead (Flat Appl) x x0) t3 H11) in (or3_ind (ex3_2 T T
+Appl) t3 t))))))) H6 (THead (Flat Appl) x x0) H3) in (let H10 \def (eq_ind T
+t2 (\lambda (t: T).(\forall (t3: T).((((eq T t t3) \to (\forall (P:
+Prop).P))) \to ((pr3 c t t3) \to (\forall (x1: T).(\forall (x2: T).((eq T t3
+(THead (Flat Appl) x1 x2)) \to (\forall (v3: T).((sn3 c v3) \to (((\forall
+(u2: T).((pr3 c t3 u2) \to ((((iso t3 u2) \to (\forall (P: Prop).P))) \to
+(sn3 c (THead (Flat Appl) v3 u2)))))) \to (sn3 c (THead (Flat Appl) v3
+t3)))))))))))) H2 (THead (Flat Appl) x x0) H3) in (let H11 \def (eq_ind T t2
+(\lambda (t: T).(\forall (t3: T).((((eq T t t3) \to (\forall (P: Prop).P)))
+\to ((pr3 c t t3) \to (sn3 c t3))))) H1 (THead (Flat Appl) x x0) H3) in
+(eq_ind_r T (THead (Flat Appl) x x0) (\lambda (t: T).(sn3 c (THead (Flat
+Appl) t0 t))) (sn3_pr2_intro c (THead (Flat Appl) t0 (THead (Flat Appl) x
+x0)) (\lambda (t3: T).(\lambda (H12: (((eq T (THead (Flat Appl) t0 (THead
+(Flat Appl) x x0)) t3) \to (\forall (P: Prop).P)))).(\lambda (H13: (pr2 c
+(THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t3)).(let H14 \def
+(pr2_gen_appl c t0 (THead (Flat Appl) x x0) t3 H13) 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 t0 u2))) (\lambda (_: T).(\lambda
(t4: T).(pr2 c (THead (Flat Appl) x x0) t4)))) (ex4_4 T T T T (\lambda (y1:
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 (H13: (ex3_2 T T (\lambda (u2:
+y2) z1 z2)))))))) (sn3 c t3) (\lambda (H15: (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 t0 u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c
(THead (Flat Appl) x 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 t0 u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Flat Appl)
-x x0) t4))) (sn3 c t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (H14: (eq T
-t3 (THead (Flat Appl) x1 x2))).(\lambda (H15: (pr2 c t0 x1)).(\lambda (H16:
-(pr2 c (THead (Flat Appl) x x0) x2)).(let H17 \def (eq_ind T t3 (\lambda (t:
+x x0) t4))) (sn3 c t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (H16: (eq T
+t3 (THead (Flat Appl) x1 x2))).(\lambda (H17: (pr2 c t0 x1)).(\lambda (H18:
+(pr2 c (THead (Flat Appl) x x0) x2)).(let H19 \def (eq_ind T t3 (\lambda (t:
T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t) \to (\forall (P:
-Prop).P))) H10 (THead (Flat Appl) x1 x2) H14) in (eq_ind_r T (THead (Flat
-Appl) x1 x2) (\lambda (t: T).(sn3 c t)) (let H18 \def (pr2_gen_appl c x x0 x2
-H16) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead
+Prop).P))) H12 (THead (Flat Appl) x1 x2) H16) in (eq_ind_r T (THead (Flat
+Appl) x1 x2) (\lambda (t: T).(sn3 c t)) (let H20 \def (pr2_gen_appl c x x0 x2
+H18) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead
(Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
(\lambda (_: T).(\lambda (t4: T).(pr2 c x0 t4)))) (ex4_4 T T T T (\lambda
(y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x0 (THead
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
-(THead (Flat Appl) x1 x2)) (\lambda (H19: (ex3_2 T T (\lambda (u2:
+(THead (Flat Appl) x1 x2)) (\lambda (H21: (ex3_2 T T (\lambda (u2:
T).(\lambda (t4: T).(eq T x2 (THead (Flat Appl) u2 t4)))) (\lambda (u2:
T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c x0
t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead
(Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
(\lambda (_: T).(\lambda (t4: T).(pr2 c x0 t4))) (sn3 c (THead (Flat Appl) x1
-x2)) (\lambda (x3: T).(\lambda (x4: T).(\lambda (H20: (eq T x2 (THead (Flat
-Appl) x3 x4))).(\lambda (H21: (pr2 c x x3)).(\lambda (H22: (pr2 c x0
-x4)).(let H23 \def (eq_ind T x2 (\lambda (t: T).((eq T (THead (Flat Appl) t0
+x2)) (\lambda (x3: T).(\lambda (x4: T).(\lambda (H22: (eq T x2 (THead (Flat
+Appl) x3 x4))).(\lambda (H23: (pr2 c x x3)).(\lambda (H24: (pr2 c x0
+x4)).(let H25 \def (eq_ind T x2 (\lambda (t: T).((eq T (THead (Flat Appl) t0
(THead (Flat Appl) x x0)) (THead (Flat Appl) x1 t)) \to (\forall (P:
-Prop).P))) H17 (THead (Flat Appl) x3 x4) H20) in (eq_ind_r T (THead (Flat
+Prop).P))) H19 (THead (Flat Appl) x3 x4) H22) in (eq_ind_r T (THead (Flat
Appl) x3 x4) (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 t))) (let H_x \def
-(term_dec (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4)) in (let H24
+(term_dec (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4)) in (let H26
\def H_x in (or_ind (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4))
((eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4)) \to (\forall (P:
Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))) (\lambda
-(H25: (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4))).(let H26
+(H27: (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4))).(let H28
\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
with [(TSort _) \Rightarrow x | (TLRef _) \Rightarrow x | (THead _ t _)
-\Rightarrow t])) (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4) H25) in
-((let H27 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_:
+\Rightarrow t])) (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4) H27) in
+((let H29 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_:
T).T) with [(TSort _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 | (THead _ _
-t) \Rightarrow t])) (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4) H25)
-in (\lambda (H28: (eq T x x3)).(let H29 \def (eq_ind_r T x4 (\lambda (t:
+t) \Rightarrow t])) (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4) H27)
+in (\lambda (H30: (eq T x x3)).(let H31 \def (eq_ind_r T x4 (\lambda (t:
T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) (THead (Flat Appl)
-x1 (THead (Flat Appl) x3 t))) \to (\forall (P: Prop).P))) H23 x0 H27) in (let
-H30 \def (eq_ind_r T x4 (\lambda (t: T).(pr2 c x0 t)) H22 x0 H27) in (eq_ind
+x1 (THead (Flat Appl) x3 t))) \to (\forall (P: Prop).P))) H25 x0 H29) in (let
+H32 \def (eq_ind_r T x4 (\lambda (t: T).(pr2 c x0 t)) H24 x0 H29) in (eq_ind
T x0 (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 t))))
-(let H31 \def (eq_ind_r T x3 (\lambda (t: T).((eq T (THead (Flat Appl) t0
+(let H33 \def (eq_ind_r T x3 (\lambda (t: T).((eq T (THead (Flat Appl) t0
(THead (Flat Appl) x x0)) (THead (Flat Appl) x1 (THead (Flat Appl) t x0)))
-\to (\forall (P: Prop).P))) H29 x H28) in (let H32 \def (eq_ind_r T x3
-(\lambda (t: T).(pr2 c x t)) H21 x H28) in (eq_ind T x (\lambda (t: T).(sn3 c
+\to (\forall (P: Prop).P))) H31 x H30) in (let H34 \def (eq_ind_r T x3
+(\lambda (t: T).(pr2 c x t)) H23 x H30) in (eq_ind T x (\lambda (t: T).(sn3 c
(THead (Flat Appl) x1 (THead (Flat Appl) t x0)))) (let H_x0 \def (term_dec t0
-x1) in (let H33 \def H_x0 in (or_ind (eq T t0 x1) ((eq T t0 x1) \to (\forall
+x1) in (let H35 \def H_x0 in (or_ind (eq T t0 x1) ((eq T t0 x1) \to (\forall
(P: Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0)))
-(\lambda (H34: (eq T t0 x1)).(let H35 \def (eq_ind_r T x1 (\lambda (t:
+(\lambda (H36: (eq T t0 x1)).(let H37 \def (eq_ind_r T x1 (\lambda (t:
T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) (THead (Flat Appl)
-t (THead (Flat Appl) x x0))) \to (\forall (P: Prop).P))) H31 t0 H34) in (let
-H36 \def (eq_ind_r T x1 (\lambda (t: T).(pr2 c t0 t)) H15 t0 H34) in (eq_ind
+t (THead (Flat Appl) x x0))) \to (\forall (P: Prop).P))) H33 t0 H36) in (let
+H38 \def (eq_ind_r T x1 (\lambda (t: T).(pr2 c t0 t)) H17 t0 H36) in (eq_ind
T t0 (\lambda (t: T).(sn3 c (THead (Flat Appl) t (THead (Flat Appl) x x0))))
-(H35 (refl_equal T (THead (Flat Appl) t0 (THead (Flat Appl) x x0))) (sn3 c
-(THead (Flat Appl) t0 (THead (Flat Appl) x x0)))) x1 H34)))) (\lambda (H34:
-(((eq T t0 x1) \to (\forall (P: Prop).P)))).(H6 x1 H34 (pr3_pr2 c t0 x1 H15)
-(\lambda (u2: T).(\lambda (H35: (pr3 c (THead (Flat Appl) x x0) u2)).(\lambda
-(H36: (((iso (THead (Flat Appl) x x0) u2) \to (\forall (P:
-Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t0 u2) (H7 u2 H35 H36) (THead
+(H37 (refl_equal T (THead (Flat Appl) t0 (THead (Flat Appl) x x0))) (sn3 c
+(THead (Flat Appl) t0 (THead (Flat Appl) x x0)))) x1 H36)))) (\lambda (H36:
+(((eq T t0 x1) \to (\forall (P: Prop).P)))).(H9 x1 H36 (pr3_pr2 c t0 x1 H17)
+(\lambda (u2: T).(\lambda (H37: (pr3 c (THead (Flat Appl) x x0) u2)).(\lambda
+(H38: (((iso (THead (Flat Appl) x x0) u2) \to (\forall (P:
+Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t0 u2) (H8 u2 H37 H38) (THead
(Flat Appl) x1 u2) (pr3_pr2 c (THead (Flat Appl) t0 u2) (THead (Flat Appl) x1
-u2) (pr2_head_1 c t0 x1 H15 (Flat Appl) u2)))))))) H33))) x3 H28))) x4
-H27))))) H26))) (\lambda (H25: (((eq T (THead (Flat Appl) x x0) (THead (Flat
-Appl) x3 x4)) \to (\forall (P: Prop).P)))).(H8 (THead (Flat Appl) x3 x4) H25
-(pr3_flat c x x3 (pr3_pr2 c x x3 H21) x0 x4 (pr3_pr2 c x0 x4 H22) Appl) x3 x4
+u2) (pr2_head_1 c t0 x1 H17 (Flat Appl) u2)))))))) H35))) x3 H30))) x4
+H29))))) H28))) (\lambda (H27: (((eq T (THead (Flat Appl) x x0) (THead (Flat
+Appl) x3 x4)) \to (\forall (P: Prop).P)))).(H10 (THead (Flat Appl) x3 x4) H27
+(pr3_flat c x x3 (pr3_pr2 c x x3 H23) x0 x4 (pr3_pr2 c x0 x4 H24) Appl) x3 x4
(refl_equal T (THead (Flat Appl) x3 x4)) x1 (sn3_pr3_trans c t0 (sn3_sing c
-t0 H5) x1 (pr3_pr2 c t0 x1 H15)) (\lambda (u2: T).(\lambda (H26: (pr3 c
-(THead (Flat Appl) x3 x4) u2)).(\lambda (H27: (((iso (THead (Flat Appl) x3
+t0 H5) x1 (pr3_pr2 c t0 x1 H17)) (\lambda (u2: T).(\lambda (H28: (pr3 c
+(THead (Flat Appl) x3 x4) u2)).(\lambda (H29: (((iso (THead (Flat Appl) x3
x4) u2) \to (\forall (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t0
-u2) (H7 u2 (pr3_sing c (THead (Flat Appl) x x4) (THead (Flat Appl) x x0)
-(pr2_thin_dx c x0 x4 H22 x Appl) u2 (pr3_sing c (THead (Flat Appl) x3 x4)
-(THead (Flat Appl) x x4) (pr2_head_1 c x x3 H21 (Flat Appl) x4) u2 H26))
-(\lambda (H28: (iso (THead (Flat Appl) x x0) u2)).(\lambda (P: Prop).(H27
+u2) (H8 u2 (pr3_sing c (THead (Flat Appl) x x4) (THead (Flat Appl) x x0)
+(pr2_thin_dx c x0 x4 H24 x Appl) u2 (pr3_sing c (THead (Flat Appl) x3 x4)
+(THead (Flat Appl) x x4) (pr2_head_1 c x x3 H23 (Flat Appl) x4) u2 H28))
+(\lambda (H30: (iso (THead (Flat Appl) x x0) u2)).(\lambda (P: Prop).(H29
(iso_trans (THead (Flat Appl) x3 x4) (THead (Flat Appl) x x0) (iso_head x3 x
-x4 x0 (Flat Appl)) u2 H28) P)))) (THead (Flat Appl) x1 u2) (pr3_pr2 c (THead
-(Flat Appl) t0 u2) (THead (Flat Appl) x1 u2) (pr2_head_1 c t0 x1 H15 (Flat
-Appl) u2)))))))) H24))) x2 H20))))))) H19)) (\lambda (H19: (ex4_4 T T T T
+x4 x0 (Flat Appl)) u2 H30) P)))) (THead (Flat Appl) x1 u2) (pr3_pr2 c (THead
+(Flat Appl) t0 u2) (THead (Flat Appl) x1 u2) (pr2_head_1 c t0 x1 H17 (Flat
+Appl) u2)))))))) H26))) x2 H22))))))) H21)) (\lambda (H21: (ex4_4 T T T T
(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x0
(THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
T).(\lambda (t4: T).(eq T x2 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
(_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b:
B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4))))))) (sn3 c (THead (Flat
Appl) x1 x2)) (\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda
-(x6: T).(\lambda (H20: (eq T x0 (THead (Bind Abst) x3 x4))).(\lambda (H21:
-(eq T x2 (THead (Bind Abbr) x5 x6))).(\lambda (H22: (pr2 c x x5)).(\lambda
-(H23: ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x4
-x6))))).(let H24 \def (eq_ind T x2 (\lambda (t: T).((eq T (THead (Flat Appl)
+(x6: T).(\lambda (H22: (eq T x0 (THead (Bind Abst) x3 x4))).(\lambda (H23:
+(eq T x2 (THead (Bind Abbr) x5 x6))).(\lambda (H24: (pr2 c x x5)).(\lambda
+(H25: ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x4
+x6))))).(let H26 \def (eq_ind T x2 (\lambda (t: T).((eq T (THead (Flat Appl)
t0 (THead (Flat Appl) x x0)) (THead (Flat Appl) x1 t)) \to (\forall (P:
-Prop).P))) H17 (THead (Bind Abbr) x5 x6) H21) in (eq_ind_r T (THead (Bind
-Abbr) x5 x6) (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 t))) (let H25 \def
+Prop).P))) H19 (THead (Bind Abbr) x5 x6) H23) in (eq_ind_r T (THead (Bind
+Abbr) x5 x6) (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 t))) (let H27 \def
(eq_ind T x0 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl)
x t)) (THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6))) \to (\forall (P:
-Prop).P))) H24 (THead (Bind Abst) x3 x4) H20) in (let H26 \def (eq_ind T x0
+Prop).P))) H26 (THead (Bind Abst) x3 x4) H22) in (let H28 \def (eq_ind T x0
(\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat Appl) x t) t4) \to
(\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x t) t4) \to (sn3 c
-t4))))) H9 (THead (Bind Abst) x3 x4) H20) in (let H27 \def (eq_ind T x0
+t4))))) H11 (THead (Bind Abst) x3 x4) H22) in (let H29 \def (eq_ind T x0
(\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat Appl) x t) t4) \to
(\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x t) t4) \to (\forall
(x7: T).(\forall (x8: T).((eq T t4 (THead (Flat Appl) x7 x8)) \to (\forall
-(v3: T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x7 x8)
-u2) \to ((((iso (THead (Flat Appl) x7 x8) u2) \to (\forall (P: Prop).P))) \to
-(sn3 c (THead (Flat Appl) v3 u2)))))) \to (sn3 c (THead (Flat Appl) v3 (THead
-(Flat Appl) x7 x8))))))))))))) H8 (THead (Bind Abst) x3 x4) H20) in (let H28
-\def (eq_ind T x0 (\lambda (t: T).(\forall (u2: T).((pr3 c (THead (Flat Appl)
-x t) u2) \to ((((iso (THead (Flat Appl) x t) u2) \to (\forall (P: Prop).P)))
-\to (sn3 c (THead (Flat Appl) t0 u2)))))) H7 (THead (Bind Abst) x3 x4) H20)
-in (let H29 \def (eq_ind T x0 (\lambda (t: T).(\forall (t4: T).((((eq T t0
-t4) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t4) \to (((\forall (u2:
-T).((pr3 c (THead (Flat Appl) x t) u2) \to ((((iso (THead (Flat Appl) x t)
-u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t4 u2)))))) \to
-(sn3 c (THead (Flat Appl) t4 (THead (Flat Appl) x t)))))))) H6 (THead (Bind
-Abst) x3 x4) H20) in (sn3_pr3_trans c (THead (Flat Appl) t0 (THead (Bind
-Abbr) x5 x6)) (H28 (THead (Bind Abbr) x5 x6) (pr3_sing c (THead (Bind Abbr) x
-x4) (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) (pr2_free c (THead (Flat
-Appl) x (THead (Bind Abst) x3 x4)) (THead (Bind Abbr) x x4) (pr0_beta x3 x x
-(pr0_refl x) x4 x4 (pr0_refl x4))) (THead (Bind Abbr) x5 x6) (pr3_head_12 c x
-x5 (pr3_pr2 c x x5 H22) (Bind Abbr) x4 x6 (pr3_pr2 (CHead c (Bind Abbr) x5)
-x4 x6 (H23 Abbr x5)))) (\lambda (H30: (iso (THead (Flat Appl) x (THead (Bind
-Abst) x3 x4)) (THead (Bind Abbr) x5 x6))).(\lambda (P: Prop).(let H31 \def
-(match H30 in iso return (\lambda (t: T).(\lambda (t4: T).(\lambda (_: (iso t
-t4)).((eq T t (THead (Flat Appl) x (THead (Bind Abst) x3 x4))) \to ((eq T t4
-(THead (Bind Abbr) x5 x6)) \to P))))) with [(iso_sort n1 n2) \Rightarrow
-(\lambda (H31: (eq T (TSort n1) (THead (Flat Appl) x (THead (Bind Abst) x3
-x4)))).(\lambda (H32: (eq T (TSort n2) (THead (Bind Abbr) x5 x6))).((let H33
-\def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
-T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
-(THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) x (THead (Bind Abst)
-x3 x4)) H31) in (False_ind ((eq T (TSort n2) (THead (Bind Abbr) x5 x6)) \to
-P) H33)) H32))) | (iso_lref i1 i2) \Rightarrow (\lambda (H31: (eq T (TLRef
-i1) (THead (Flat Appl) x (THead (Bind Abst) x3 x4)))).(\lambda (H32: (eq T
-(TLRef i2) (THead (Bind Abbr) x5 x6))).((let H33 \def (eq_ind T (TLRef i1)
-(\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
-\Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
-False])) I (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) H31) in (False_ind
-((eq T (TLRef i2) (THead (Bind Abbr) x5 x6)) \to P) H33)) H32))) | (iso_head
-v4 v5 t4 t5 k) \Rightarrow (\lambda (H31: (eq T (THead k v4 t4) (THead (Flat
-Appl) x (THead (Bind Abst) x3 x4)))).(\lambda (H32: (eq T (THead k v5 t5)
-(THead (Bind Abbr) x5 x6))).((let H33 \def (f_equal T T (\lambda (e:
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t4 |
-(TLRef _) \Rightarrow t4 | (THead _ _ t) \Rightarrow t])) (THead k v4 t4)
-(THead (Flat Appl) x (THead (Bind Abst) x3 x4)) H31) in ((let H34 \def
-(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
-[(TSort _) \Rightarrow v4 | (TLRef _) \Rightarrow v4 | (THead _ t _)
-\Rightarrow t])) (THead k v4 t4) (THead (Flat Appl) x (THead (Bind Abst) x3
-x4)) H31) in ((let H35 \def (f_equal T K (\lambda (e: T).(match e in T return
-(\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k |
-(THead k0 _ _) \Rightarrow k0])) (THead k v4 t4) (THead (Flat Appl) x (THead
-(Bind Abst) x3 x4)) H31) in (eq_ind K (Flat Appl) (\lambda (k0: K).((eq T v4
-x) \to ((eq T t4 (THead (Bind Abst) x3 x4)) \to ((eq T (THead k0 v5 t5)
-(THead (Bind Abbr) x5 x6)) \to P)))) (\lambda (H36: (eq T v4 x)).(eq_ind T x
-(\lambda (_: T).((eq T t4 (THead (Bind Abst) x3 x4)) \to ((eq T (THead (Flat
-Appl) v5 t5) (THead (Bind Abbr) x5 x6)) \to P))) (\lambda (H37: (eq T t4
-(THead (Bind Abst) x3 x4))).(eq_ind T (THead (Bind Abst) x3 x4) (\lambda (_:
-T).((eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6)) \to P))
-(\lambda (H38: (eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5
-x6))).(let H39 \def (eq_ind T (THead (Flat Appl) v5 t5) (\lambda (e:
-T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
-False | (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in
-K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _)
-\Rightarrow True])])) I (THead (Bind Abbr) x5 x6) H38) in (False_ind P H39)))
-t4 (sym_eq T t4 (THead (Bind Abst) x3 x4) H37))) v4 (sym_eq T v4 x H36))) k
-(sym_eq K k (Flat Appl) H35))) H34)) H33)) H32)))]) in (H31 (refl_equal T
-(THead (Flat Appl) x (THead (Bind Abst) x3 x4))) (refl_equal T (THead (Bind
-Abbr) x5 x6))))))) (THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6)) (pr3_pr2
-c (THead (Flat Appl) t0 (THead (Bind Abbr) x5 x6)) (THead (Flat Appl) x1
-(THead (Bind Abbr) x5 x6)) (pr2_head_1 c t0 x1 H15 (Flat Appl) (THead (Bind
-Abbr) x5 x6))))))))) x2 H21)))))))))) H19)) (\lambda (H19: (ex6_6 B T T T T T
-(\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
+(v3: T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c t4 u2) \to ((((iso t4 u2)
+\to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v3 u2)))))) \to
+(sn3 c (THead (Flat Appl) v3 t4)))))))))))) H10 (THead (Bind Abst) x3 x4)
+H22) in (let H30 \def (eq_ind T x0 (\lambda (t: T).(\forall (u2: T).((pr3 c
+(THead (Flat Appl) x t) u2) \to ((((iso (THead (Flat Appl) x t) u2) \to
+(\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t0 u2)))))) H8 (THead
+(Bind Abst) x3 x4) H22) in (let H31 \def (eq_ind T x0 (\lambda (t:
+T).(\forall (t4: T).((((eq T t0 t4) \to (\forall (P: Prop).P))) \to ((pr3 c
+t0 t4) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x t) u2) \to ((((iso
+(THead (Flat Appl) x t) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
+(Flat Appl) t4 u2)))))) \to (sn3 c (THead (Flat Appl) t4 (THead (Flat Appl) x
+t)))))))) H9 (THead (Bind Abst) x3 x4) H22) in (sn3_pr3_trans c (THead (Flat
+Appl) t0 (THead (Bind Abbr) x5 x6)) (H30 (THead (Bind Abbr) x5 x6) (pr3_sing
+c (THead (Bind Abbr) x x4) (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
+(pr2_free c (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) (THead (Bind
+Abbr) x x4) (pr0_beta x3 x x (pr0_refl x) x4 x4 (pr0_refl x4))) (THead (Bind
+Abbr) x5 x6) (pr3_head_12 c x x5 (pr3_pr2 c x x5 H24) (Bind Abbr) x4 x6
+(pr3_pr2 (CHead c (Bind Abbr) x5) x4 x6 (H25 Abbr x5)))) (\lambda (H32: (iso
+(THead (Flat Appl) x (THead (Bind Abst) x3 x4)) (THead (Bind Abbr) x5
+x6))).(\lambda (P: Prop).(let H33 \def (match H32 in iso return (\lambda (t:
+T).(\lambda (t4: T).(\lambda (_: (iso t t4)).((eq T t (THead (Flat Appl) x
+(THead (Bind Abst) x3 x4))) \to ((eq T t4 (THead (Bind Abbr) x5 x6)) \to
+P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H33: (eq T (TSort n1)
+(THead (Flat Appl) x (THead (Bind Abst) x3 x4)))).(\lambda (H34: (eq T (TSort
+n2) (THead (Bind Abbr) x5 x6))).((let H35 \def (eq_ind T (TSort n1) (\lambda
+(e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
+True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I
+(THead (Flat Appl) x (THead (Bind Abst) x3 x4)) H33) in (False_ind ((eq T
+(TSort n2) (THead (Bind Abbr) x5 x6)) \to P) H35)) H34))) | (iso_lref i1 i2)
+\Rightarrow (\lambda (H33: (eq T (TLRef i1) (THead (Flat Appl) x (THead (Bind
+Abst) x3 x4)))).(\lambda (H34: (eq T (TLRef i2) (THead (Bind Abbr) x5
+x6))).((let H35 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T
+return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) x
+(THead (Bind Abst) x3 x4)) H33) in (False_ind ((eq T (TLRef i2) (THead (Bind
+Abbr) x5 x6)) \to P) H35)) H34))) | (iso_head v4 v5 t4 t5 k) \Rightarrow
+(\lambda (H33: (eq T (THead k v4 t4) (THead (Flat Appl) x (THead (Bind Abst)
+x3 x4)))).(\lambda (H34: (eq T (THead k v5 t5) (THead (Bind Abbr) x5
+x6))).((let H35 \def (f_equal T T (\lambda (e: T).(match e in T return
+(\lambda (_: T).T) with [(TSort _) \Rightarrow t4 | (TLRef _) \Rightarrow t4
+| (THead _ _ t) \Rightarrow t])) (THead k v4 t4) (THead (Flat Appl) x (THead
+(Bind Abst) x3 x4)) H33) in ((let H36 \def (f_equal T T (\lambda (e:
+T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v4 |
+(TLRef _) \Rightarrow v4 | (THead _ t _) \Rightarrow t])) (THead k v4 t4)
+(THead (Flat Appl) x (THead (Bind Abst) x3 x4)) H33) in ((let H37 \def
+(f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with
+[(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _)
+\Rightarrow k0])) (THead k v4 t4) (THead (Flat Appl) x (THead (Bind Abst) x3
+x4)) H33) in (eq_ind K (Flat Appl) (\lambda (k0: K).((eq T v4 x) \to ((eq T
+t4 (THead (Bind Abst) x3 x4)) \to ((eq T (THead k0 v5 t5) (THead (Bind Abbr)
+x5 x6)) \to P)))) (\lambda (H38: (eq T v4 x)).(eq_ind T x (\lambda (_:
+T).((eq T t4 (THead (Bind Abst) x3 x4)) \to ((eq T (THead (Flat Appl) v5 t5)
+(THead (Bind Abbr) x5 x6)) \to P))) (\lambda (H39: (eq T t4 (THead (Bind
+Abst) x3 x4))).(eq_ind T (THead (Bind Abst) x3 x4) (\lambda (_: T).((eq T
+(THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6)) \to P)) (\lambda (H40:
+(eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6))).(let H41 \def
+(eq_ind T (THead (Flat Appl) v5 t5) (\lambda (e: T).(match e in T return
+(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K return (\lambda
+(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
+True])])) I (THead (Bind Abbr) x5 x6) H40) in (False_ind P H41))) t4 (sym_eq
+T t4 (THead (Bind Abst) x3 x4) H39))) v4 (sym_eq T v4 x H38))) k (sym_eq K k
+(Flat Appl) H37))) H36)) H35)) H34)))]) in (H33 (refl_equal T (THead (Flat
+Appl) x (THead (Bind Abst) x3 x4))) (refl_equal T (THead (Bind Abbr) x5
+x6))))))) (THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6)) (pr3_pr2 c (THead
+(Flat Appl) t0 (THead (Bind Abbr) x5 x6)) (THead (Flat Appl) x1 (THead (Bind
+Abbr) x5 x6)) (pr2_head_1 c t0 x1 H17 (Flat Appl) (THead (Bind Abbr) x5
+x6))))))))) x2 H23)))))))))) H21)) (\lambda (H21: (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 x0
(THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
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 (THead (Flat Appl) x1 x2)) (\lambda (x3: B).(\lambda (x4: T).(\lambda
-(x5: T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (x8: T).(\lambda (H20:
-(not (eq B x3 Abst))).(\lambda (H21: (eq T x0 (THead (Bind x3) x4
-x5))).(\lambda (H22: (eq T x2 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S
-O) O x7) x6)))).(\lambda (H23: (pr2 c x x7)).(\lambda (H24: (pr2 c x4
-x8)).(\lambda (H25: (pr2 (CHead c (Bind x3) x8) x5 x6)).(let H26 \def (eq_ind
+(x5: T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (x8: T).(\lambda (H22:
+(not (eq B x3 Abst))).(\lambda (H23: (eq T x0 (THead (Bind x3) x4
+x5))).(\lambda (H24: (eq T x2 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S
+O) O x7) x6)))).(\lambda (H25: (pr2 c x x7)).(\lambda (H26: (pr2 c x4
+x8)).(\lambda (H27: (pr2 (CHead c (Bind x3) x8) x5 x6)).(let H28 \def (eq_ind
T x2 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0))
-(THead (Flat Appl) x1 t)) \to (\forall (P: Prop).P))) H17 (THead (Bind x3) x8
-(THead (Flat Appl) (lift (S O) O x7) x6)) H22) in (eq_ind_r T (THead (Bind
+(THead (Flat Appl) x1 t)) \to (\forall (P: Prop).P))) H19 (THead (Bind x3) x8
+(THead (Flat Appl) (lift (S O) O x7) x6)) H24) in (eq_ind_r T (THead (Bind
x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)) (\lambda (t: T).(sn3 c
-(THead (Flat Appl) x1 t))) (let H27 \def (eq_ind T x0 (\lambda (t: T).((eq T
+(THead (Flat Appl) x1 t))) (let H29 \def (eq_ind T x0 (\lambda (t: T).((eq T
(THead (Flat Appl) t0 (THead (Flat Appl) x t)) (THead (Flat Appl) x1 (THead
(Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))) \to (\forall (P:
-Prop).P))) H26 (THead (Bind x3) x4 x5) H21) in (let H28 \def (eq_ind T x0
+Prop).P))) H28 (THead (Bind x3) x4 x5) H23) in (let H30 \def (eq_ind T x0
(\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat Appl) x t) t4) \to
(\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x t) t4) \to (sn3 c
-t4))))) H9 (THead (Bind x3) x4 x5) H21) in (let H29 \def (eq_ind T x0
+t4))))) H11 (THead (Bind x3) x4 x5) H23) in (let H31 \def (eq_ind T x0
(\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat Appl) x t) t4) \to
(\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x t) t4) \to (\forall
(x9: T).(\forall (x10: T).((eq T t4 (THead (Flat Appl) x9 x10)) \to (\forall
-(v3: T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x9 x10)
-u2) \to ((((iso (THead (Flat Appl) x9 x10) u2) \to (\forall (P: Prop).P)))
-\to (sn3 c (THead (Flat Appl) v3 u2)))))) \to (sn3 c (THead (Flat Appl) v3
-(THead (Flat Appl) x9 x10))))))))))))) H8 (THead (Bind x3) x4 x5) H21) in
-(let H30 \def (eq_ind T x0 (\lambda (t: T).(\forall (u2: T).((pr3 c (THead
+(v3: T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c t4 u2) \to ((((iso t4 u2)
+\to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v3 u2)))))) \to
+(sn3 c (THead (Flat Appl) v3 t4)))))))))))) H10 (THead (Bind x3) x4 x5) H23)
+in (let H32 \def (eq_ind T x0 (\lambda (t: T).(\forall (u2: T).((pr3 c (THead
(Flat Appl) x t) u2) \to ((((iso (THead (Flat Appl) x t) u2) \to (\forall (P:
-Prop).P))) \to (sn3 c (THead (Flat Appl) t0 u2)))))) H7 (THead (Bind x3) x4
-x5) H21) in (let H31 \def (eq_ind T x0 (\lambda (t: T).(\forall (t4:
+Prop).P))) \to (sn3 c (THead (Flat Appl) t0 u2)))))) H8 (THead (Bind x3) x4
+x5) H23) in (let H33 \def (eq_ind T x0 (\lambda (t: T).(\forall (t4:
T).((((eq T t0 t4) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t4) \to
(((\forall (u2: T).((pr3 c (THead (Flat Appl) x t) u2) \to ((((iso (THead
(Flat Appl) x t) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat
Appl) t4 u2)))))) \to (sn3 c (THead (Flat Appl) t4 (THead (Flat Appl) x
-t)))))))) H6 (THead (Bind x3) x4 x5) H21) in (sn3_pr3_trans c (THead (Flat
-Appl) t0 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) (H30
+t)))))))) H9 (THead (Bind x3) x4 x5) H23) in (sn3_pr3_trans c (THead (Flat
+Appl) t0 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) (H32
(THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)) (pr3_sing c
(THead (Bind x3) x4 (THead (Flat Appl) (lift (S O) O x) x5)) (THead (Flat
Appl) x (THead (Bind x3) x4 x5)) (pr2_free c (THead (Flat Appl) x (THead
(Bind x3) x4 x5)) (THead (Bind x3) x4 (THead (Flat Appl) (lift (S O) O x)
-x5)) (pr0_upsilon x3 H20 x x (pr0_refl x) x4 x4 (pr0_refl x4) x5 x5 (pr0_refl
+x5)) (pr0_upsilon x3 H22 x x (pr0_refl x) x4 x4 (pr0_refl x4) x5 x5 (pr0_refl
x5))) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
-(pr3_head_12 c x4 x8 (pr3_pr2 c x4 x8 H24) (Bind x3) (THead (Flat Appl) (lift
+(pr3_head_12 c x4 x8 (pr3_pr2 c x4 x8 H26) (Bind x3) (THead (Flat Appl) (lift
(S O) O x) x5) (THead (Flat Appl) (lift (S O) O x7) x6) (pr3_head_12 (CHead c
(Bind x3) x8) (lift (S O) O x) (lift (S O) O x7) (pr3_lift (CHead c (Bind x3)
x8) c (S O) O (drop_drop (Bind x3) O c c (drop_refl c) x8) x x7 (pr3_pr2 c x
-x7 H23)) (Flat Appl) x5 x6 (pr3_pr2 (CHead (CHead c (Bind x3) x8) (Flat Appl)
-(lift (S O) O x7)) x5 x6 (pr2_cflat (CHead c (Bind x3) x8) x5 x6 H25 Appl
-(lift (S O) O x7)))))) (\lambda (H32: (iso (THead (Flat Appl) x (THead (Bind
+x7 H25)) (Flat Appl) x5 x6 (pr3_pr2 (CHead (CHead c (Bind x3) x8) (Flat Appl)
+(lift (S O) O x7)) x5 x6 (pr2_cflat (CHead c (Bind x3) x8) x5 x6 H27 Appl
+(lift (S O) O x7)))))) (\lambda (H34: (iso (THead (Flat Appl) x (THead (Bind
x3) x4 x5)) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7)
-x6)))).(\lambda (P: Prop).(let H33 \def (match H32 in iso return (\lambda (t:
+x6)))).(\lambda (P: Prop).(let H35 \def (match H34 in iso return (\lambda (t:
T).(\lambda (t4: T).(\lambda (_: (iso t t4)).((eq T t (THead (Flat Appl) x
(THead (Bind x3) x4 x5))) \to ((eq T t4 (THead (Bind x3) x8 (THead (Flat
Appl) (lift (S O) O x7) x6))) \to P))))) with [(iso_sort n1 n2) \Rightarrow
-(\lambda (H33: (eq T (TSort n1) (THead (Flat Appl) x (THead (Bind x3) x4
-x5)))).(\lambda (H34: (eq T (TSort n2) (THead (Bind x3) x8 (THead (Flat Appl)
-(lift (S O) O x7) x6)))).((let H35 \def (eq_ind T (TSort n1) (\lambda (e:
+(\lambda (H35: (eq T (TSort n1) (THead (Flat Appl) x (THead (Bind x3) x4
+x5)))).(\lambda (H36: (eq T (TSort n2) (THead (Bind x3) x8 (THead (Flat Appl)
+(lift (S O) O x7) x6)))).((let H37 \def (eq_ind T (TSort n1) (\lambda (e:
T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I
-(THead (Flat Appl) x (THead (Bind x3) x4 x5)) H33) in (False_ind ((eq T
+(THead (Flat Appl) x (THead (Bind x3) x4 x5)) H35) in (False_ind ((eq T
(TSort n2) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to
-P) H35)) H34))) | (iso_lref i1 i2) \Rightarrow (\lambda (H33: (eq T (TLRef
-i1) (THead (Flat Appl) x (THead (Bind x3) x4 x5)))).(\lambda (H34: (eq T
+P) H37)) H36))) | (iso_lref i1 i2) \Rightarrow (\lambda (H35: (eq T (TLRef
+i1) (THead (Flat Appl) x (THead (Bind x3) x4 x5)))).(\lambda (H36: (eq T
(TLRef i2) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7)
-x6)))).((let H35 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T
+x6)))).((let H37 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T
return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) x
-(THead (Bind x3) x4 x5)) H33) in (False_ind ((eq T (TLRef i2) (THead (Bind
-x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to P) H35)) H34))) |
-(iso_head v4 v5 t4 t5 k) \Rightarrow (\lambda (H33: (eq T (THead k v4 t4)
-(THead (Flat Appl) x (THead (Bind x3) x4 x5)))).(\lambda (H34: (eq T (THead k
+(THead (Bind x3) x4 x5)) H35) in (False_ind ((eq T (TLRef i2) (THead (Bind
+x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to P) H37)) H36))) |
+(iso_head v4 v5 t4 t5 k) \Rightarrow (\lambda (H35: (eq T (THead k v4 t4)
+(THead (Flat Appl) x (THead (Bind x3) x4 x5)))).(\lambda (H36: (eq T (THead k
v5 t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))).((let
-H35 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
+H37 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
with [(TSort _) \Rightarrow t4 | (TLRef _) \Rightarrow t4 | (THead _ _ t)
\Rightarrow t])) (THead k v4 t4) (THead (Flat Appl) x (THead (Bind x3) x4
-x5)) H33) in ((let H36 \def (f_equal T T (\lambda (e: T).(match e in T return
+x5)) H35) in ((let H38 \def (f_equal T T (\lambda (e: T).(match e in T return
(\lambda (_: T).T) with [(TSort _) \Rightarrow v4 | (TLRef _) \Rightarrow v4
| (THead _ t _) \Rightarrow t])) (THead k v4 t4) (THead (Flat Appl) x (THead
-(Bind x3) x4 x5)) H33) in ((let H37 \def (f_equal T K (\lambda (e: T).(match
+(Bind x3) x4 x5)) H35) in ((let H39 \def (f_equal T K (\lambda (e: T).(match
e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
\Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k v4 t4) (THead (Flat
-Appl) x (THead (Bind x3) x4 x5)) H33) in (eq_ind K (Flat Appl) (\lambda (k0:
+Appl) x (THead (Bind x3) x4 x5)) H35) in (eq_ind K (Flat Appl) (\lambda (k0:
K).((eq T v4 x) \to ((eq T t4 (THead (Bind x3) x4 x5)) \to ((eq T (THead k0
v5 t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to
-P)))) (\lambda (H38: (eq T v4 x)).(eq_ind T x (\lambda (_: T).((eq T t4
+P)))) (\lambda (H40: (eq T v4 x)).(eq_ind T x (\lambda (_: T).((eq T t4
(THead (Bind x3) x4 x5)) \to ((eq T (THead (Flat Appl) v5 t5) (THead (Bind
-x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to P))) (\lambda (H39: (eq
+x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to P))) (\lambda (H41: (eq
T t4 (THead (Bind x3) x4 x5))).(eq_ind T (THead (Bind x3) x4 x5) (\lambda (_:
T).((eq T (THead (Flat Appl) v5 t5) (THead (Bind x3) x8 (THead (Flat Appl)
-(lift (S O) O x7) x6))) \to P)) (\lambda (H40: (eq T (THead (Flat Appl) v5
-t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))).(let H41
+(lift (S O) O x7) x6))) \to P)) (\lambda (H42: (eq T (THead (Flat Appl) v5
+t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))).(let H43
\def (eq_ind T (THead (Flat Appl) v5 t5) (\lambda (e: T).(match e in T return
(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
\Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K return (\lambda
(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
True])])) I (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
-H40) in (False_ind P H41))) t4 (sym_eq T t4 (THead (Bind x3) x4 x5) H39))) v4
-(sym_eq T v4 x H38))) k (sym_eq K k (Flat Appl) H37))) H36)) H35)) H34)))])
-in (H33 (refl_equal T (THead (Flat Appl) x (THead (Bind x3) x4 x5)))
+H42) in (False_ind P H43))) t4 (sym_eq T t4 (THead (Bind x3) x4 x5) H41))) v4
+(sym_eq T v4 x H40))) k (sym_eq K k (Flat Appl) H39))) H38)) H37)) H36)))])
+in (H35 (refl_equal T (THead (Flat Appl) x (THead (Bind x3) x4 x5)))
(refl_equal T (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7)
x6)))))))) (THead (Flat Appl) x1 (THead (Bind x3) x8 (THead (Flat Appl) (lift
(S O) O x7) x6))) (pr3_pr2 c (THead (Flat Appl) t0 (THead (Bind x3) x8 (THead
(Flat Appl) (lift (S O) O x7) x6))) (THead (Flat Appl) x1 (THead (Bind x3) x8
-(THead (Flat Appl) (lift (S O) O x7) x6))) (pr2_head_1 c t0 x1 H15 (Flat
+(THead (Flat Appl) (lift (S O) O x7) x6))) (pr2_head_1 c t0 x1 H17 (Flat
Appl) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))))))))))
-x2 H22)))))))))))))) H19)) H18)) t3 H14))))))) H13)) (\lambda (H13: (ex4_4 T
+x2 H24)))))))))))))) H21)) H20)) t3 H16))))))) H15)) (\lambda (H15: (ex4_4 T
T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
(THead (Flat Appl) x x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind
T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 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))))))) (sn3 c t3) (\lambda (x1:
-T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (H14: (eq T
-(THead (Flat Appl) x x0) (THead (Bind Abst) x1 x2))).(\lambda (H15: (eq T t3
+T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (H16: (eq T
+(THead (Flat Appl) x x0) (THead (Bind Abst) x1 x2))).(\lambda (H17: (eq T t3
(THead (Bind Abbr) x3 x4))).(\lambda (_: (pr2 c t0 x3)).(\lambda (_:
((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x2 x4))))).(let
-H18 \def (eq_ind T t3 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead
-(Flat Appl) x x0)) t) \to (\forall (P: Prop).P))) H10 (THead (Bind Abbr) x3
-x4) H15) in (eq_ind_r T (THead (Bind Abbr) x3 x4) (\lambda (t: T).(sn3 c t))
-(let H19 \def (eq_ind T (THead (Flat Appl) x x0) (\lambda (ee: T).(match ee
+H20 \def (eq_ind T t3 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead
+(Flat Appl) x x0)) t) \to (\forall (P: Prop).P))) H12 (THead (Bind Abbr) x3
+x4) H17) in (eq_ind_r T (THead (Bind Abbr) x3 x4) (\lambda (t: T).(sn3 c t))
+(let H21 \def (eq_ind T (THead (Flat Appl) x x0) (\lambda (ee: T).(match ee
in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef
_) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
(\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
-True])])) I (THead (Bind Abst) x1 x2) H14) in (False_ind (sn3 c (THead (Bind
-Abbr) x3 x4)) H19)) t3 H15)))))))))) H13)) (\lambda (H13: (ex6_6 B T T T T T
+True])])) I (THead (Bind Abst) x1 x2) H16) in (False_ind (sn3 c (THead (Bind
+Abbr) x3 x4)) H21)) t3 H17)))))))))) H15)) (\lambda (H15: (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
(\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 (x1: B).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda
-(x5: T).(\lambda (x6: T).(\lambda (_: (not (eq B x1 Abst))).(\lambda (H15:
-(eq T (THead (Flat Appl) x x0) (THead (Bind x1) x2 x3))).(\lambda (H16: (eq T
+(x5: T).(\lambda (x6: T).(\lambda (_: (not (eq B x1 Abst))).(\lambda (H17:
+(eq T (THead (Flat Appl) x x0) (THead (Bind x1) x2 x3))).(\lambda (H18: (eq T
t3 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)))).(\lambda
(_: (pr2 c t0 x5)).(\lambda (_: (pr2 c x2 x6)).(\lambda (_: (pr2 (CHead c
-(Bind x1) x6) x3 x4)).(let H20 \def (eq_ind T t3 (\lambda (t: T).((eq T
+(Bind x1) x6) x3 x4)).(let H22 \def (eq_ind T t3 (\lambda (t: T).((eq T
(THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t) \to (\forall (P:
-Prop).P))) H10 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
-H16) in (eq_ind_r T (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5)
-x4)) (\lambda (t: T).(sn3 c t)) (let H21 \def (eq_ind T (THead (Flat Appl) x
+Prop).P))) H12 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
+H18) in (eq_ind_r T (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5)
+x4)) (\lambda (t: T).(sn3 c t)) (let H23 \def (eq_ind T (THead (Flat Appl) x
x0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
_) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind x1) x2 x3)
-H15) in (False_ind (sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O)
-O x5) x4))) H21)) t3 H16)))))))))))))) H13)) H12)))))))))))) v2 H4))))))))) y
-H0))))) H))))).
+H17) in (False_ind (sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O)
+O x5) x4))) H23)) t3 H18)))))))))))))) H15)) H14)))))) t2 H3))))))))) v2
+H4))))))))) y H0))))) H))))).
theorem sn3_appl_beta:
\forall (c: C).(\forall (u: T).(\forall (v: T).(\forall (t: T).((sn3 c
projects / helm.git / blobdiff