update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / pr2 / clen.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr2/clen.ma b/matita/matita/contribs/lambdadelta/basic_1/pr2/clen.ma
index df9ea1fd97862a973cf92a6e8f585b29f148d838..b518e4360fc92acbc7ab326af7b7a3ea91486495 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/pr2/clen.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pr2/clen.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/pr2/props.ma".
+include "basic_1/pr2/props.ma".
 
-include "Basic-1/clen/getl.ma".
+include "basic_1/clen/getl.ma".
 
-theorem pr2_gen_ctail:
+lemma pr2_gen_ctail:
  \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall 
 (t2: T).((pr2 (CTail k u c) t1 t2) \to (or (pr2 c t1 t2) (ex3 T (\lambda (_: 
 T).(eq K k (Bind Abbr))) (\lambda (t: T).(pr0 t1 t)) (\lambda (t: T).(subst0 
@@ -75,11 +75,8 @@ t))) (ex3_intro T (\lambda (_: T).(eq K (Bind Abbr) (Bind Abbr))) (\lambda
 (t0: T).(pr0 t3 t0)) (\lambda (t0: T).(subst0 (clen c) u t0 t)) t4 
 (refl_equal K (Bind Abbr)) H2 H13)) k H9)))))))) H7)) H6))))))))))))))) y t1 
 t2 H0))) H)))))).
-(* COMMENTS
-Initial nodes: 1161
-END *)
 
-theorem pr2_gen_cbind:
+lemma pr2_gen_cbind:
  \forall (b: B).(\forall (c: C).(\forall (v: T).(\forall (t1: T).(\forall 
 (t2: T).((pr2 (CHead c (Bind b) v) t1 t2) \to (pr2 c (THead (Bind b) v t1) 
 (THead (Bind b) v t2)))))))
@@ -107,36 +104,32 @@ j))) (\lambda (j: nat).(getl j c (CHead d (Bind Abbr) u)))) (pr2 c (THead
 (CHead d (Bind Abbr) u) (CHead c (Bind b) v)) (pr2 c (THead (Bind b) v t3) 
 (THead (Bind b) v t)) (\lambda (H8: (eq nat i O)).(\lambda (H9: (eq C (CHead 
 d (Bind Abbr) u) (CHead c (Bind b) v))).(let H10 \def (f_equal C C (\lambda 
-(e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d 
-| (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abbr) u) (CHead c (Bind b) 
-v) H9) in ((let H11 \def (f_equal C B (\lambda (e: C).(match e in C return 
-(\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _) 
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b0) 
-\Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) 
-(CHead c (Bind b) v) H9) in ((let H12 \def (f_equal C T (\lambda (e: 
-C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | 
-(CHead _ _ t0) \Rightarrow t0])) (CHead d (Bind Abbr) u) (CHead c (Bind b) v) 
-H9) in (\lambda (H13: (eq B Abbr b)).(\lambda (_: (eq C d c)).(let H15 \def 
-(eq_ind nat i (\lambda (n: nat).(subst0 n u t4 t)) H3 O H8) in (let H16 \def 
-(eq_ind T u (\lambda (t0: T).(subst0 O t0 t4 t)) H15 v H12) in (eq_ind B Abbr 
-(\lambda (b0: B).(pr2 c (THead (Bind b0) v t3) (THead (Bind b0) v t))) 
-(pr2_free c (THead (Bind Abbr) v t3) (THead (Bind Abbr) v t) (pr0_delta v v 
-(pr0_refl v) t3 t4 H2 t H16)) b H13)))))) H11)) H10)))) H7)) (\lambda (H7: 
-(ex2 nat (\lambda (j: nat).(eq nat i (S j))) (\lambda (j: nat).(getl j c 
-(CHead d (Bind Abbr) u))))).(ex2_ind nat (\lambda (j: nat).(eq nat i (S j))) 
-(\lambda (j: nat).(getl j c (CHead d (Bind Abbr) u))) (pr2 c (THead (Bind b) 
-v t3) (THead (Bind b) v t)) (\lambda (x: nat).(\lambda (H8: (eq nat i (S 
-x))).(\lambda (H9: (getl x c (CHead d (Bind Abbr) u))).(let H10 \def (f_equal 
-nat nat (\lambda (e: nat).e) i (S x) H8) in (let H11 \def (eq_ind nat i 
-(\lambda (n: nat).(subst0 n u t4 t)) H3 (S x) H10) in (pr2_head_2 c v t3 t 
-(Bind b) (pr2_delta (CHead c (Bind b) v) d u (S x) (getl_clear_bind b (CHead 
-c (Bind b) v) c v (clear_bind b c v) (CHead d (Bind Abbr) u) x H9) t3 t4 H2 t 
-H11))))))) H7)) H6))))))))))))))) y t1 t2 H0))) H)))))).
-(* COMMENTS
-Initial nodes: 1085
-END *)
+(e: C).(match e with [(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow 
+c1])) (CHead d (Bind Abbr) u) (CHead c (Bind b) v) H9) in ((let H11 \def 
+(f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow Abbr | 
+(CHead _ k _) \Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _) 
+\Rightarrow Abbr])])) (CHead d (Bind Abbr) u) (CHead c (Bind b) v) H9) in 
+((let H12 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d (Bind Abbr) u) 
+(CHead c (Bind b) v) H9) in (\lambda (H13: (eq B Abbr b)).(\lambda (_: (eq C 
+d c)).(let H15 \def (eq_ind nat i (\lambda (n: nat).(subst0 n u t4 t)) H3 O 
+H8) in (let H16 \def (eq_ind T u (\lambda (t0: T).(subst0 O t0 t4 t)) H15 v 
+H12) in (eq_ind B Abbr (\lambda (b0: B).(pr2 c (THead (Bind b0) v t3) (THead 
+(Bind b0) v t))) (pr2_free c (THead (Bind Abbr) v t3) (THead (Bind Abbr) v t) 
+(pr0_delta v v (pr0_refl v) t3 t4 H2 t H16)) b H13)))))) H11)) H10)))) H7)) 
+(\lambda (H7: (ex2 nat (\lambda (j: nat).(eq nat i (S j))) (\lambda (j: 
+nat).(getl j c (CHead d (Bind Abbr) u))))).(ex2_ind nat (\lambda (j: nat).(eq 
+nat i (S j))) (\lambda (j: nat).(getl j c (CHead d (Bind Abbr) u))) (pr2 c 
+(THead (Bind b) v t3) (THead (Bind b) v t)) (\lambda (x: nat).(\lambda (H8: 
+(eq nat i (S x))).(\lambda (H9: (getl x c (CHead d (Bind Abbr) u))).(let H10 
+\def (f_equal nat nat (\lambda (e: nat).e) i (S x) H8) in (let H11 \def 
+(eq_ind nat i (\lambda (n: nat).(subst0 n u t4 t)) H3 (S x) H10) in 
+(pr2_head_2 c v t3 t (Bind b) (pr2_delta (CHead c (Bind b) v) d u (S x) 
+(getl_clear_bind b (CHead c (Bind b) v) c v (clear_bind b c v) (CHead d (Bind 
+Abbr) u) x H9) t3 t4 H2 t H11))))))) H7)) H6))))))))))))))) y t1 t2 H0))) 
+H)))))).
 
-theorem pr2_gen_cflat:
+lemma pr2_gen_cflat:
  \forall (f: F).(\forall (c: C).(\forall (v: T).(\forall (t1: T).(\forall 
 (t2: T).((pr2 (CHead c (Flat f) v) t1 t2) \to (pr2 c t1 t2))))))
 \def
@@ -155,7 +148,4 @@ T).(\lambda (t4: T).(\lambda (H2: (pr0 t3 t4)).(\lambda (t: T).(\lambda (H3:
 c (Flat f) v) H4) in (let H_y \def (getl_gen_flat f c (CHead d (Bind Abbr) u) 
 v i H5) in (pr2_delta c d u i H_y t3 t4 H2 t H3)))))))))))))) y t1 t2 H0))) 
 H)))))).
-(* COMMENTS
-Initial nodes: 293
-END *)