X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fsn3%2Fprops.ma;h=ec20b825f722e54c02f8f25c6b52596355352e43;hb=6329f0f87906d3347c39d2ba2f5ec2b2124f17a2;hp=b47e2a185ce67e142bcdd65159ffbee70c8d830f;hpb=783fbc6eb42d5db260d93d8d213a7d5c035e99e3;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma
index b47e2a185..ec20b825f 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-
+set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/props".
 
 include "sn3/nf2.ma".
 
@@ -322,79 +322,79 @@ t)) \to (\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat Appl) v (THead
 \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 
@@ -740,13 +740,13 @@ theorem sn3_appl_abbr:
  \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 
@@ -928,28 +928,29 @@ u)) \to (\forall (t: T).((sn3 c (THead (Flat Appl) v t)) \to (sn3 c (THead
 \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 
@@ -1201,38 +1202,38 @@ Appl) (lift (S O) O v) t)) \to (sn3 c (THead (Flat Appl) v (THead (Bind b) t2
 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 (_: 
@@ -1637,60 +1638,61 @@ u1)))))))))
 \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: 
@@ -1711,19 +1713,19 @@ T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 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 (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 
@@ -1743,69 +1745,69 @@ B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: 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 
-(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 (_: 
@@ -1819,91 +1821,91 @@ 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))))))) (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 (_: 
@@ -1926,109 +1928,108 @@ 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 (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 
@@ -2042,19 +2043,19 @@ T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_:
 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 
@@ -2079,22 +2080,22 @@ 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 (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