X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fpr0%2Fdec.ma;h=35f388d279659da2104ecac22fed7eccbc7c42a7;hb=f73bd1c1cdd504c2a991071505b2e4f541791a7f;hp=429de32f7b9fe38ab7bed7422e6b48374ead1f07;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma
index 429de32f7..35f388d27 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma
@@ -14,15 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+include "LambdaDelta-1/pr0/fwd.ma".
 
+include "LambdaDelta-1/subst0/dec.ma".
 
-include "pr0/fwd.ma".
+include "LambdaDelta-1/T/dec.ma".
 
-include "subst0/dec.ma".
-
-include "T/dec.ma".
-
-include "T/props.ma".
+include "LambdaDelta-1/T/props.ma".
 
 theorem nf0_dec:
  \forall (t1: T).(or (\forall (t2: T).((pr0 t1 t2) \to (eq T t1 t2))) (ex2 T 
@@ -205,7 +203,7 @@ H10 \def (eq_ind T t0 (\lambda (t3: T).(subst0 O t t3 (lift (S O) O x))) H3
 (lift (S O) O t2) H_y) in (eq_ind_r T (lift (S O) O t2) (\lambda (t3: T).(eq 
 T (THead (Bind Void) t t3) t2)) (subst0_gen_lift_false t2 t (lift (S O) O x) 
 (S O) O O (le_n O) (eq_ind_r nat (plus (S O) O) (\lambda (n: nat).(lt O n)) 
-(le_n (plus (S O) O)) (plus O (S O)) (plus_comm O (S O))) H10 (eq T (THead 
+(le_n (plus (S O) O)) (plus O (S O)) (plus_sym O (S O))) H10 (eq T (THead 
 (Bind Void) t (lift (S O) O t2)) t2)) t0 H_y)))) (pr0_gen_void t t0 t2 
 H8)))))) (\lambda (H7: (ex2 T (\lambda (t2: T).((eq T t0 t2) \to (\forall (P: 
 Prop).P))) (\lambda (t2: T).(pr0 t0 t2)))).(ex2_ind T (\lambda (t2: T).((eq T 
@@ -264,36 +262,36 @@ O) O x)) t2))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Bind Void) t
 (lift (S O) O x)) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 
 (THead (Bind Void) t (lift (S O) O x)) t2)) x (\lambda (H5: (eq T (THead 
 (Bind Void) t (lift (S O) O x)) x)).(\lambda (P: Prop).(thead_x_lift_y_y 
-(Bind Void) x t (S O) O H5 P))) (pr0_zeta Void not_void_abst x x (pr0_refl x) 
-t))) t0 H3))) H2))) H1))) b)) (\lambda (f: F).(F_ind (\lambda (f0: F).(or 
-(\forall (t2: T).((pr0 (THead (Flat f0) t t0) t2) \to (eq T (THead (Flat f0) 
-t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat f0) t t0) t2) \to 
-(\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat f0) t t0) t2))))) 
-(let H_x \def (binder_dec t0) in (let H1 \def H_x in (or_ind (ex_3 B T T 
+(Bind Void) x t (S O) O H5 P))) (pr0_zeta Void (sym_not_eq B Abst Void 
+not_abst_void) x x (pr0_refl x) t))) t0 H3))) H2))) H1))) b)) (\lambda (f: 
+F).(F_ind (\lambda (f0: F).(or (\forall (t2: T).((pr0 (THead (Flat f0) t t0) 
+t2) \to (eq T (THead (Flat f0) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T 
+(THead (Flat f0) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 
+(THead (Flat f0) t t0) t2))))) (let H_x \def (binder_dec t0) in (let H1 \def 
+H_x in (or_ind (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: 
+T).(eq T t0 (THead (Bind b) w u)))))) (\forall (b: B).(\forall (w: 
+T).(\forall (u: T).((eq T t0 (THead (Bind b) w u)) \to (\forall (P: 
+Prop).P))))) (or (\forall (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq 
+T (THead (Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat 
+Appl) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead 
+(Flat Appl) t t0) t2)))) (\lambda (H2: (ex_3 B T T (\lambda (b: B).(\lambda 
+(w: T).(\lambda (u: T).(eq T t0 (THead (Bind b) w u))))))).(ex_3_ind B T T 
 (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T t0 (THead (Bind b) w 
-u)))))) (\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t0 (THead 
-(Bind b) w u)) \to (\forall (P: Prop).P))))) (or (\forall (t2: T).((pr0 
-(THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T 
-(\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P: 
-Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2)))) (\lambda 
-(H2: (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: T).(eq T t0 
-(THead (Bind b) w u))))))).(ex_3_ind B T T (\lambda (b: B).(\lambda (w: 
-T).(\lambda (u: T).(eq T t0 (THead (Bind b) w u))))) (or (\forall (t2: 
-T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) 
-t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to 
-(\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2)))) 
-(\lambda (x0: B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (H3: (eq T t0 
-(THead (Bind x0) x1 x2))).(let H4 \def (eq_ind T t0 (\lambda (t2: T).(or 
-(\forall (t3: T).((pr0 t2 t3) \to (eq T t2 t3))) (ex2 T (\lambda (t3: T).((eq 
-T t2 t3) \to (\forall (P: Prop).P))) (\lambda (t3: T).(pr0 t2 t3))))) H0 
-(THead (Bind x0) x1 x2) H3) in (eq_ind_r T (THead (Bind x0) x1 x2) (\lambda 
-(t2: T).(or (\forall (t3: T).((pr0 (THead (Flat Appl) t t2) t3) \to (eq T 
-(THead (Flat Appl) t t2) t3))) (ex2 T (\lambda (t3: T).((eq T (THead (Flat 
-Appl) t t2) t3) \to (\forall (P: Prop).P))) (\lambda (t3: T).(pr0 (THead 
-(Flat Appl) t t2) t3))))) (B_ind (\lambda (b: B).((or (\forall (t2: T).((pr0 
-(THead (Bind b) x1 x2) t2) \to (eq T (THead (Bind b) x1 x2) t2))) (ex2 T 
-(\lambda (t2: T).((eq T (THead (Bind b) x1 x2) t2) \to (\forall (P: 
-Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind b) x1 x2) t2)))) \to (or 
+u))))) (or (\forall (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T 
+(THead (Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat 
+Appl) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead 
+(Flat Appl) t t0) t2)))) (\lambda (x0: B).(\lambda (x1: T).(\lambda (x2: 
+T).(\lambda (H3: (eq T t0 (THead (Bind x0) x1 x2))).(let H4 \def (eq_ind T t0 
+(\lambda (t2: T).(or (\forall (t3: T).((pr0 t2 t3) \to (eq T t2 t3))) (ex2 T 
+(\lambda (t3: T).((eq T t2 t3) \to (\forall (P: Prop).P))) (\lambda (t3: 
+T).(pr0 t2 t3))))) H0 (THead (Bind x0) x1 x2) H3) in (eq_ind_r T (THead (Bind 
+x0) x1 x2) (\lambda (t2: T).(or (\forall (t3: T).((pr0 (THead (Flat Appl) t 
+t2) t3) \to (eq T (THead (Flat Appl) t t2) t3))) (ex2 T (\lambda (t3: T).((eq 
+T (THead (Flat Appl) t t2) t3) \to (\forall (P: Prop).P))) (\lambda (t3: 
+T).(pr0 (THead (Flat Appl) t t2) t3))))) (B_ind (\lambda (b: B).((or (\forall 
+(t2: T).((pr0 (THead (Bind b) x1 x2) t2) \to (eq T (THead (Bind b) x1 x2) 
+t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Bind b) x1 x2) t2) \to (\forall 
+(P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Bind b) x1 x2) t2)))) \to (or 
 (\forall (t2: T).((pr0 (THead (Flat Appl) t (THead (Bind b) x1 x2)) t2) \to 
 (eq T (THead (Flat Appl) t (THead (Bind b) x1 x2)) t2))) (ex2 T (\lambda (t2: 
 T).((eq T (THead (Flat Appl) t (THead (Bind b) x1 x2)) t2) \to (\forall (P: 
@@ -359,95 +357,35 @@ Prop).(let H7 \def (eq_ind T (THead (Flat Appl) t (THead (Bind Void) x1 x2))
 | (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K 
 return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) 
 \Rightarrow False])])])) I (THead (Bind Void) x1 (THead (Flat Appl) (lift (S 
-O) O t) x2)) H6) in (False_ind P H7)))) (pr0_upsilon Void not_void_abst t t 
-(pr0_refl t) x1 x1 (pr0_refl x1) x2 x2 (pr0_refl x2))))) x0 H4) t0 H3)))))) 
-H2)) (\lambda (H2: ((\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t0 
-(THead (Bind b) w u)) \to (\forall (P: Prop).P))))))).(let H3 \def H in 
-(or_ind (\forall (t2: T).((pr0 t t2) \to (eq T t t2))) (ex2 T (\lambda (t2: 
-T).((eq T t t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2))) (or 
-(\forall (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat 
-Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) 
-\to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) 
-t2)))) (\lambda (H4: ((\forall (t2: T).((pr0 t t2) \to (eq T t t2))))).(let 
-H5 \def H0 in (or_ind (\forall (t2: T).((pr0 t0 t2) \to (eq T t0 t2))) (ex2 T 
-(\lambda (t2: T).((eq T t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: 
-T).(pr0 t0 t2))) (or (\forall (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to 
-(eq T (THead (Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead 
-(Flat Appl) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 
-(THead (Flat Appl) t t0) t2)))) (\lambda (H6: ((\forall (t2: T).((pr0 t0 t2) 
-\to (eq T t0 t2))))).(or_introl (\forall (t2: T).((pr0 (THead (Flat Appl) t 
+O) O t) x2)) H6) in (False_ind P H7)))) (pr0_upsilon Void (sym_not_eq B Abst 
+Void not_abst_void) t t (pr0_refl t) x1 x1 (pr0_refl x1) x2 x2 (pr0_refl 
+x2))))) x0 H4) t0 H3)))))) H2)) (\lambda (H2: ((\forall (b: B).(\forall (w: 
+T).(\forall (u: T).((eq T t0 (THead (Bind b) w u)) \to (\forall (P: 
+Prop).P))))))).(let H3 \def H in (or_ind (\forall (t2: T).((pr0 t t2) \to (eq 
+T t t2))) (ex2 T (\lambda (t2: T).((eq T t t2) \to (\forall (P: Prop).P))) 
+(\lambda (t2: T).(pr0 t t2))) (or (\forall (t2: T).((pr0 (THead (Flat Appl) t 
 t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq 
 T (THead (Flat Appl) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: 
-T).(pr0 (THead (Flat Appl) t t0) t2))) (\lambda (t2: T).(\lambda (H7: (pr0 
-(THead (Flat Appl) t t0) t2)).(or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda 
-(t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: 
-T).(pr0 t u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t0 t3)))) (ex4_4 T T T 
-T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t0 
-(THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: 
-T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: 
-T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 t u2))))) (\lambda 
-(_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3)))))) 
-(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 t0 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: 
-T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T 
-t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t3))))))))) 
-(\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: 
-T).(\lambda (_: T).(pr0 t u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda 
-(_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) 
-(\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: 
-T).(\lambda (t3: T).(pr0 z1 t3)))))))) (eq T (THead (Flat Appl) t t0) t2) 
-(\lambda (H8: (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead 
-(Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 t u2))) (\lambda 
-(_: T).(\lambda (t3: T).(pr0 t0 t3))))).(ex3_2_ind T T (\lambda (u2: 
-T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: 
-T).(\lambda (_: T).(pr0 t u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t0 
-t3))) (eq T (THead (Flat Appl) t t0) t2) (\lambda (x0: T).(\lambda (x1: 
-T).(\lambda (H9: (eq T t2 (THead (Flat Appl) x0 x1))).(\lambda (H10: (pr0 t 
-x0)).(\lambda (H11: (pr0 t0 x1)).(let H_y \def (H6 x1 H11) in (let H_y0 \def 
-(H4 x0 H10) in (let H12 \def (eq_ind_r T x1 (\lambda (t3: T).(pr0 t0 t3)) H11 
-t0 H_y) in (let H13 \def (eq_ind_r T x1 (\lambda (t3: T).(eq T t2 (THead 
-(Flat Appl) x0 t3))) H9 t0 H_y) in (let H14 \def (eq_ind_r T x0 (\lambda (t3: 
-T).(pr0 t t3)) H10 t H_y0) in (let H15 \def (eq_ind_r T x0 (\lambda (t3: 
-T).(eq T t2 (THead (Flat Appl) t3 t0))) H13 t H_y0) in (eq_ind_r T (THead 
-(Flat Appl) t t0) (\lambda (t3: T).(eq T (THead (Flat Appl) t t0) t3)) 
-(refl_equal T (THead (Flat Appl) t t0)) t2 H15)))))))))))) H8)) (\lambda (H8: 
-(ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: 
-T).(eq T t0 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: 
-T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) 
-(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 t 
-u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: 
-T).(pr0 z1 t3))))))).(ex4_4_ind T T T T (\lambda (y1: T).(\lambda (z1: 
+T).(pr0 (THead (Flat Appl) t t0) t2)))) (\lambda (H4: ((\forall (t2: T).((pr0 
+t t2) \to (eq T t t2))))).(let H5 \def H0 in (or_ind (\forall (t2: T).((pr0 
+t0 t2) \to (eq T t0 t2))) (ex2 T (\lambda (t2: T).((eq T t0 t2) \to (\forall 
+(P: Prop).P))) (\lambda (t2: T).(pr0 t0 t2))) (or (\forall (t2: T).((pr0 
+(THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T 
+(\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P: 
+Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2)))) (\lambda 
+(H6: ((\forall (t2: T).((pr0 t0 t2) \to (eq T t0 t2))))).(or_introl (\forall 
+(t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) 
+t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to 
+(\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2))) 
+(\lambda (t2: T).(\lambda (H7: (pr0 (THead (Flat Appl) t t0) t2)).(or3_ind 
+(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 
+t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 t u2))) (\lambda (_: T).(\lambda 
+(t3: T).(pr0 t0 t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: 
 T).(\lambda (_: T).(\lambda (_: T).(eq T t0 (THead (Bind Abst) y1 z1)))))) 
 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 
 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: 
 T).(\lambda (_: T).(pr0 t u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda 
-(_: T).(\lambda (t3: T).(pr0 z1 t3))))) (eq T (THead (Flat Appl) t t0) t2) 
-(\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda 
-(H9: (eq T t0 (THead (Bind Abst) x0 x1))).(\lambda (H10: (eq T t2 (THead 
-(Bind Abbr) x2 x3))).(\lambda (_: (pr0 t x2)).(\lambda (_: (pr0 x1 
-x3)).(eq_ind_r T (THead (Bind Abbr) x2 x3) (\lambda (t3: T).(eq T (THead 
-(Flat Appl) t t0) t3)) (let H13 \def (eq_ind T t0 (\lambda (t3: T).(\forall 
-(t4: T).((pr0 t3 t4) \to (eq T t3 t4)))) H6 (THead (Bind Abst) x0 x1) H9) in 
-(let H14 \def (eq_ind T t0 (\lambda (t3: T).(\forall (b: B).(\forall (w: 
-T).(\forall (u: T).((eq T t3 (THead (Bind b) w u)) \to (\forall (P: 
-Prop).P)))))) H2 (THead (Bind Abst) x0 x1) H9) in (eq_ind_r T (THead (Bind 
-Abst) x0 x1) (\lambda (t3: T).(eq T (THead (Flat Appl) t t3) (THead (Bind 
-Abbr) x2 x3))) (H14 Abst x0 x1 (H13 (THead (Bind Abst) x0 x1) (pr0_refl 
-(THead (Bind Abst) x0 x1))) (eq T (THead (Flat Appl) t (THead (Bind Abst) x0 
-x1)) (THead (Bind Abbr) x2 x3))) t0 H9))) t2 H10))))))))) H8)) (\lambda (H8: 
-(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 t0 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: 
-T).(\lambda (_: T).(\lambda (u2: T).(\lambda (v2: T).(\lambda (t3: T).(eq T 
-t2 (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O u2) t3))))))))) 
-(\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: 
-T).(\lambda (_: T).(pr0 t u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda 
-(_: T).(\lambda (_: T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) 
-(\lambda (_: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: 
-T).(\lambda (t3: T).(pr0 z1 t3))))))))).(ex6_6_ind B T T T T T (\lambda (b: 
+(_: T).(\lambda (t3: T).(pr0 z1 t3)))))) (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 t0 (THead (Bind 
@@ -458,51 +396,111 @@ T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 t
 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: 
 T).(\lambda (v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_: 
 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda 
-(t3: T).(pr0 z1 t3))))))) (eq T (THead (Flat Appl) t t0) t2) (\lambda (x0: 
-B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: 
-T).(\lambda (x5: T).(\lambda (_: (not (eq B x0 Abst))).(\lambda (H10: (eq T 
-t0 (THead (Bind x0) x1 x2))).(\lambda (H11: (eq T t2 (THead (Bind x0) x4 
-(THead (Flat Appl) (lift (S O) O x3) x5)))).(\lambda (_: (pr0 t x3)).(\lambda 
-(_: (pr0 x1 x4)).(\lambda (_: (pr0 x2 x5)).(eq_ind_r T (THead (Bind x0) x4 
-(THead (Flat Appl) (lift (S O) O x3) x5)) (\lambda (t3: T).(eq T (THead (Flat 
-Appl) t t0) t3)) (let H15 \def (eq_ind T t0 (\lambda (t3: T).(\forall (t4: 
-T).((pr0 t3 t4) \to (eq T t3 t4)))) H6 (THead (Bind x0) x1 x2) H10) in (let 
-H16 \def (eq_ind T t0 (\lambda (t3: T).(\forall (b: B).(\forall (w: 
-T).(\forall (u: T).((eq T t3 (THead (Bind b) w u)) \to (\forall (P: 
-Prop).P)))))) H2 (THead (Bind x0) x1 x2) H10) in (eq_ind_r T (THead (Bind x0) 
-x1 x2) (\lambda (t3: T).(eq T (THead (Flat Appl) t t3) (THead (Bind x0) x4 
-(THead (Flat Appl) (lift (S O) O x3) x5)))) (H16 x0 x1 x2 (H15 (THead (Bind 
-x0) x1 x2) (pr0_refl (THead (Bind x0) x1 x2))) (eq T (THead (Flat Appl) t 
-(THead (Bind x0) x1 x2)) (THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O 
-x3) x5)))) t0 H10))) t2 H11))))))))))))) H8)) (pr0_gen_appl t t0 t2 H7)))))) 
-(\lambda (H6: (ex2 T (\lambda (t2: T).((eq T t0 t2) \to (\forall (P: 
-Prop).P))) (\lambda (t2: T).(pr0 t0 t2)))).(ex2_ind T (\lambda (t2: T).((eq T 
-t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t0 t2)) (or (\forall 
-(t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) 
-t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to 
-(\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2)))) 
-(\lambda (x: T).(\lambda (H7: (((eq T t0 x) \to (\forall (P: 
-Prop).P)))).(\lambda (H8: (pr0 t0 x)).(or_intror (\forall (t2: T).((pr0 
-(THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T 
-(\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P: 
-Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2))) (ex_intro2 T 
-(\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P: 
-Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2)) (THead (Flat 
-Appl) t x) (\lambda (H9: (eq T (THead (Flat Appl) t t0) (THead (Flat Appl) t 
-x))).(\lambda (P: Prop).(let H10 \def (f_equal T T (\lambda (e: T).(match e 
-in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) 
-\Rightarrow t0 | (THead _ _ t2) \Rightarrow t2])) (THead (Flat Appl) t t0) 
-(THead (Flat Appl) t x) H9) in (let H11 \def (eq_ind_r T x (\lambda (t2: 
-T).(pr0 t0 t2)) H8 t0 H10) in (let H12 \def (eq_ind_r T x (\lambda (t2: 
-T).((eq T t0 t2) \to (\forall (P0: Prop).P0))) H7 t0 H10) in (H12 (refl_equal 
-T t0) P)))))) (pr0_comp t t (pr0_refl t) t0 x H8 (Flat Appl))))))) H6)) H5))) 
-(\lambda (H4: (ex2 T (\lambda (t2: T).((eq T t t2) \to (\forall (P: 
-Prop).P))) (\lambda (t2: T).(pr0 t t2)))).(ex2_ind T (\lambda (t2: T).((eq T 
-t t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2)) (or (\forall 
-(t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) 
-t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to 
-(\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2)))) 
-(\lambda (x: T).(\lambda (H5: (((eq T t x) \to (\forall (P: 
+(t3: T).(pr0 z1 t3)))))))) (eq T (THead (Flat Appl) t t0) t2) (\lambda (H8: 
+(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 
+t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 t u2))) (\lambda (_: T).(\lambda 
+(t3: T).(pr0 t0 t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq 
+T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 t 
+u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t0 t3))) (eq T (THead (Flat Appl) 
+t t0) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H9: (eq T t2 (THead 
+(Flat Appl) x0 x1))).(\lambda (H10: (pr0 t x0)).(\lambda (H11: (pr0 t0 
+x1)).(let H_y \def (H6 x1 H11) in (let H_y0 \def (H4 x0 H10) in (let H12 \def 
+(eq_ind_r T x1 (\lambda (t3: T).(pr0 t0 t3)) H11 t0 H_y) in (let H13 \def 
+(eq_ind_r T x1 (\lambda (t3: T).(eq T t2 (THead (Flat Appl) x0 t3))) H9 t0 
+H_y) in (let H14 \def (eq_ind_r T x0 (\lambda (t3: T).(pr0 t t3)) H10 t H_y0) 
+in (let H15 \def (eq_ind_r T x0 (\lambda (t3: T).(eq T t2 (THead (Flat Appl) 
+t3 t0))) H13 t H_y0) in (eq_ind_r T (THead (Flat Appl) t t0) (\lambda (t3: 
+T).(eq T (THead (Flat Appl) t t0) t3)) (refl_equal T (THead (Flat Appl) t 
+t0)) t2 H15)))))))))))) H8)) (\lambda (H8: (ex4_4 T T T T (\lambda (y1: 
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t0 (THead (Bind 
+Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda 
+(t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: 
+T).(\lambda (u2: T).(\lambda (_: T).(pr0 t u2))))) (\lambda (_: T).(\lambda 
+(z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))))).(ex4_4_ind T T T T 
+(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T t0 
+(THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: 
+T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: 
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr0 t u2))))) (\lambda 
+(_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))) (eq 
+T (THead (Flat Appl) t t0) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda 
+(x2: T).(\lambda (x3: T).(\lambda (H9: (eq T t0 (THead (Bind Abst) x0 
+x1))).(\lambda (H10: (eq T t2 (THead (Bind Abbr) x2 x3))).(\lambda (_: (pr0 t 
+x2)).(\lambda (_: (pr0 x1 x3)).(eq_ind_r T (THead (Bind Abbr) x2 x3) (\lambda 
+(t3: T).(eq T (THead (Flat Appl) t t0) t3)) (let H13 \def (eq_ind T t0 
+(\lambda (t3: T).(\forall (t4: T).((pr0 t3 t4) \to (eq T t3 t4)))) H6 (THead 
+(Bind Abst) x0 x1) H9) in (let H14 \def (eq_ind T t0 (\lambda (t3: 
+T).(\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t3 (THead (Bind b) 
+w u)) \to (\forall (P: Prop).P)))))) H2 (THead (Bind Abst) x0 x1) H9) in 
+(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t3: T).(eq T (THead (Flat 
+Appl) t t3) (THead (Bind Abbr) x2 x3))) (H14 Abst x0 x1 (H13 (THead (Bind 
+Abst) x0 x1) (pr0_refl (THead (Bind Abst) x0 x1))) (eq T (THead (Flat Appl) t 
+(THead (Bind Abst) x0 x1)) (THead (Bind Abbr) x2 x3))) t0 H9))) t2 
+H10))))))))) H8)) (\lambda (H8: (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 t0 (THead (Bind b) 
+y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: 
+T).(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind b) v2 (THead (Flat 
+Appl) (lift (S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda 
+(_: T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 t u2))))))) 
+(\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda 
+(v2: T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_: B).(\lambda (_: 
+T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 
+t3))))))))).(ex6_6_ind 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 t0 (THead (Bind b) y1 z1)))))))) 
+(\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda 
+(v2: T).(\lambda (t3: T).(eq T t2 (THead (Bind b) v2 (THead (Flat Appl) (lift 
+(S O) O u2) t3))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: 
+T).(\lambda (u2: T).(\lambda (_: T).(\lambda (_: T).(pr0 t u2))))))) (\lambda 
+(_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (v2: 
+T).(\lambda (_: T).(pr0 y1 v2))))))) (\lambda (_: B).(\lambda (_: T).(\lambda 
+(z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (t3: T).(pr0 z1 t3))))))) 
+(eq T (THead (Flat Appl) t t0) t2) (\lambda (x0: B).(\lambda (x1: T).(\lambda 
+(x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (not 
+(eq B x0 Abst))).(\lambda (H10: (eq T t0 (THead (Bind x0) x1 x2))).(\lambda 
+(H11: (eq T t2 (THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O x3) 
+x5)))).(\lambda (_: (pr0 t x3)).(\lambda (_: (pr0 x1 x4)).(\lambda (_: (pr0 
+x2 x5)).(eq_ind_r T (THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O x3) 
+x5)) (\lambda (t3: T).(eq T (THead (Flat Appl) t t0) t3)) (let H15 \def 
+(eq_ind T t0 (\lambda (t3: T).(\forall (t4: T).((pr0 t3 t4) \to (eq T t3 
+t4)))) H6 (THead (Bind x0) x1 x2) H10) in (let H16 \def (eq_ind T t0 (\lambda 
+(t3: T).(\forall (b: B).(\forall (w: T).(\forall (u: T).((eq T t3 (THead 
+(Bind b) w u)) \to (\forall (P: Prop).P)))))) H2 (THead (Bind x0) x1 x2) H10) 
+in (eq_ind_r T (THead (Bind x0) x1 x2) (\lambda (t3: T).(eq T (THead (Flat 
+Appl) t t3) (THead (Bind x0) x4 (THead (Flat Appl) (lift (S O) O x3) x5)))) 
+(H16 x0 x1 x2 (H15 (THead (Bind x0) x1 x2) (pr0_refl (THead (Bind x0) x1 
+x2))) (eq T (THead (Flat Appl) t (THead (Bind x0) x1 x2)) (THead (Bind x0) x4 
+(THead (Flat Appl) (lift (S O) O x3) x5)))) t0 H10))) t2 H11))))))))))))) 
+H8)) (pr0_gen_appl t t0 t2 H7)))))) (\lambda (H6: (ex2 T (\lambda (t2: 
+T).((eq T t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t0 
+t2)))).(ex2_ind T (\lambda (t2: T).((eq T t0 t2) \to (\forall (P: Prop).P))) 
+(\lambda (t2: T).(pr0 t0 t2)) (or (\forall (t2: T).((pr0 (THead (Flat Appl) t 
+t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq 
+T (THead (Flat Appl) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: 
+T).(pr0 (THead (Flat Appl) t t0) t2)))) (\lambda (x: T).(\lambda (H7: (((eq T 
+t0 x) \to (\forall (P: Prop).P)))).(\lambda (H8: (pr0 t0 x)).(or_intror 
+(\forall (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead (Flat 
+Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) 
+\to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) 
+t2))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to 
+(\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) t t0) t2)) 
+(THead (Flat Appl) t x) (\lambda (H9: (eq T (THead (Flat Appl) t t0) (THead 
+(Flat Appl) t x))).(\lambda (P: Prop).(let H10 \def (f_equal T T (\lambda (e: 
+T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | 
+(TLRef _) \Rightarrow t0 | (THead _ _ t2) \Rightarrow t2])) (THead (Flat 
+Appl) t t0) (THead (Flat Appl) t x) H9) in (let H11 \def (eq_ind_r T x 
+(\lambda (t2: T).(pr0 t0 t2)) H8 t0 H10) in (let H12 \def (eq_ind_r T x 
+(\lambda (t2: T).((eq T t0 t2) \to (\forall (P0: Prop).P0))) H7 t0 H10) in 
+(H12 (refl_equal T t0) P)))))) (pr0_comp t t (pr0_refl t) t0 x H8 (Flat 
+Appl))))))) H6)) H5))) (\lambda (H4: (ex2 T (\lambda (t2: T).((eq T t t2) \to 
+(\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2)))).(ex2_ind T (\lambda 
+(t2: T).((eq T t t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t t2)) 
+(or (\forall (t2: T).((pr0 (THead (Flat Appl) t t0) t2) \to (eq T (THead 
+(Flat Appl) t t0) t2))) (ex2 T (\lambda (t2: T).((eq T (THead (Flat Appl) t 
+t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead (Flat Appl) 
+t t0) t2)))) (\lambda (x: T).(\lambda (H5: (((eq T t x) \to (\forall (P: 
 Prop).P)))).(\lambda (H6: (pr0 t x)).(or_intror (\forall (t2: T).((pr0 (THead 
 (Flat Appl) t t0) t2) \to (eq T (THead (Flat Appl) t t0) t2))) (ex2 T 
 (\lambda (t2: T).((eq T (THead (Flat Appl) t t0) t2) \to (\forall (P: 
@@ -523,6 +521,6 @@ Cast) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead
 (Flat Cast) t t0) t2))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Flat 
 Cast) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead 
 (Flat Cast) t t0) t2)) t0 (\lambda (H1: (eq T (THead (Flat Cast) t t0) 
-t0)).(\lambda (P: Prop).(thead_x_y_y (Flat Cast) t t0 H1 P))) (pr0_epsilon t0 
-t0 (pr0_refl t0) t))) f)) k)))))) t1).
+t0)).(\lambda (P: Prop).(thead_x_y_y (Flat Cast) t t0 H1 P))) (pr0_tau t0 t0 
+(pr0_refl t0) t))) f)) k)))))) t1).