update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / nf2 / props.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/nf2/props.ma b/matita/matita/contribs/lambdadelta/basic_1/nf2/props.ma
index 2f0f092f2cd4bf6ebc030b7bf622076824530ad0..ccaa9eb52f74dfb852210fb6a06751f7ce0b7023 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/nf2/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/nf2/props.ma
@@ -14,21 +14,18 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/nf2/defs.ma".
+include "basic_1/nf2/defs.ma".
 
-include "Basic-1/pr2/fwd.ma".
+include "basic_1/pr2/fwd.ma".
 
-theorem nf2_sort:
+lemma nf2_sort:
  \forall (c: C).(\forall (n: nat).(nf2 c (TSort n)))
 \def
  \lambda (c: C).(\lambda (n: nat).(\lambda (t2: T).(\lambda (H: (pr2 c (TSort 
 n) t2)).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (TSort n) t)) (refl_equal 
 T (TSort n)) t2 (pr2_gen_sort c t2 n H))))).
-(* COMMENTS
-Initial nodes: 55
-END *)
 
-theorem nf2_csort_lref:
+lemma nf2_csort_lref:
  \forall (n: nat).(\forall (i: nat).(nf2 (CSort n) (TLRef i)))
 \def
  \lambda (n: nat).(\lambda (i: nat).(\lambda (t2: T).(\lambda (H: (pr2 (CSort 
@@ -46,9 +43,6 @@ n) (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift
 (lift (S i) O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T 
 (TLRef i) t)) (getl_gen_sort n i (CHead x0 (Bind Abbr) x1) H2 (eq T (TLRef i) 
 (lift (S i) O x1))) t2 H3))))) H1)) H0))))).
-(* COMMENTS
-Initial nodes: 355
-END *)
 
 theorem nf2_abst:
  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (b: B).(\forall (v: 
@@ -70,9 +64,6 @@ x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T (THead
 (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst) u x0 t 
 x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 b v))) t2 H3)))))) 
 H2)))))))))).
-(* COMMENTS
-Initial nodes: 299
-END *)
 
 theorem nf2_abst_shift:
  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (t: T).((nf2 (CHead c 
@@ -92,11 +83,8 @@ b) u0) t x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T
 (THead (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst) 
 u x0 t x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 Abst u))) t2 
 H3)))))) H2)))))))).
-(* COMMENTS
-Initial nodes: 295
-END *)
 
-theorem nfs2_tapp:
+lemma nfs2_tapp:
  \forall (c: C).(\forall (t: T).(\forall (ts: TList).((nfs2 c (TApp ts t)) 
 \to (land (nfs2 c ts) (nf2 c t)))))
 \def
@@ -113,11 +101,8 @@ H4 \def H_x in (land_ind (nfs2 c t1) (nf2 c t) (land (land (nf2 c t0) (nfs2 c
 t1)) (nf2 c t)) (\lambda (H5: (nfs2 c t1)).(\lambda (H6: (nf2 c t)).(conj 
 (land (nf2 c t0) (nfs2 c t1)) (nf2 c t) (conj (nf2 c t0) (nfs2 c t1) H2 H5) 
 H6))) H4))))) H1)))))) ts))).
-(* COMMENTS
-Initial nodes: 295
-END *)
 
-theorem nf2_appls_lref:
+lemma nf2_appls_lref:
  \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (vs: 
 TList).((nfs2 c vs) \to (nf2 c (THeads (Flat Appl) vs (TLRef i)))))))
 \def
@@ -197,38 +182,37 @@ u) x1 x3))))).(eq_ind_r T (THead (Bind Abbr) x2 x3) (\lambda (t1: T).(eq T
 (Flat Appl) t (THeads (Flat Appl) t1 (TLRef i))) (THead (Bind Abbr) x2 
 x3))))) (\lambda (_: (nf2 c (THeads (Flat Appl) TNil (TLRef i)))).(\lambda 
 (H13: (eq T (THeads (Flat Appl) TNil (TLRef i)) (THead (Bind Abst) x0 
-x1))).(let H14 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T 
-return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
-\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) x0 
-x1) H13) in (False_ind (eq T (THead (Flat Appl) t (THeads (Flat Appl) TNil 
-(TLRef i))) (THead (Bind Abbr) x2 x3)) H14)))) (\lambda (t1: T).(\lambda (t3: 
-TList).(\lambda (_: (((nf2 c (THeads (Flat Appl) t3 (TLRef i))) \to ((eq T 
-(THeads (Flat Appl) t3 (TLRef i)) (THead (Bind Abst) x0 x1)) \to (eq T (THead 
-(Flat Appl) t (THeads (Flat Appl) t3 (TLRef i))) (THead (Bind Abbr) x2 
-x3)))))).(\lambda (_: (nf2 c (THeads (Flat Appl) (TCons t1 t3) (TLRef 
-i)))).(\lambda (H13: (eq T (THeads (Flat Appl) (TCons t1 t3) (TLRef i)) 
-(THead (Bind Abst) x0 x1))).(let H14 \def (eq_ind T (THead (Flat Appl) t1 
-(THeads (Flat Appl) t3 (TLRef i))) (\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) x0 x1) H13) in (False_ind (eq T (THead (Flat 
-Appl) t (THeads (Flat Appl) (TCons t1 t3) (TLRef i))) (THead (Bind Abbr) x2 
-x3)) H14))))))) t0 H_y H8) t2 H9))))))))) H7)) (\lambda (H7: (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 (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind b) y1 z1)))))))) (\lambda 
-(b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: 
-T).(\lambda (y2: T).(eq T t2 (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 t 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))))))))).(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 (_: 
+x1))).(let H14 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee with 
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) 
+\Rightarrow False])) I (THead (Bind Abst) x0 x1) H13) in (False_ind (eq T 
+(THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))) (THead (Bind Abbr) 
+x2 x3)) H14)))) (\lambda (t1: T).(\lambda (t3: TList).(\lambda (_: (((nf2 c 
+(THeads (Flat Appl) t3 (TLRef i))) \to ((eq T (THeads (Flat Appl) t3 (TLRef 
+i)) (THead (Bind Abst) x0 x1)) \to (eq T (THead (Flat Appl) t (THeads (Flat 
+Appl) t3 (TLRef i))) (THead (Bind Abbr) x2 x3)))))).(\lambda (_: (nf2 c 
+(THeads (Flat Appl) (TCons t1 t3) (TLRef i)))).(\lambda (H13: (eq T (THeads 
+(Flat Appl) (TCons t1 t3) (TLRef i)) (THead (Bind Abst) x0 x1))).(let H14 
+\def (eq_ind T (THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i))) 
+(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _) 
+\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) x0 
+x1) H13) in (False_ind (eq T (THead (Flat Appl) t (THeads (Flat Appl) (TCons 
+t1 t3) (TLRef i))) (THead (Bind Abbr) x2 x3)) H14))))))) t0 H_y H8) t2 
+H9))))))))) H7)) (\lambda (H7: (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 (THeads (Flat Appl) 
+t0 (TLRef i)) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: 
+T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T 
+t2 (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 t 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))))))))).(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 (THeads (Flat Appl) t0 (TLRef i)) 
 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: 
 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind 
@@ -253,28 +237,23 @@ Appl) t1 (TLRef i)) (THead (Bind x0) x1 x2)) \to (eq T (THead (Flat Appl) t
 (lift (S O) O x4) x3)))))) (\lambda (_: (nf2 c (THeads (Flat Appl) TNil 
 (TLRef i)))).(\lambda (H15: (eq T (THeads (Flat Appl) TNil (TLRef i)) (THead 
 (Bind x0) x1 x2))).(let H16 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match 
-ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | 
-(TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead 
-(Bind x0) x1 x2) H15) in (False_ind (eq T (THead (Flat Appl) t (THeads (Flat 
-Appl) TNil (TLRef i))) (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O 
-x4) x3))) H16)))) (\lambda (t1: T).(\lambda (t3: TList).(\lambda (_: (((nf2 c 
-(THeads (Flat Appl) t3 (TLRef i))) \to ((eq T (THeads (Flat Appl) t3 (TLRef 
-i)) (THead (Bind x0) x1 x2)) \to (eq T (THead (Flat Appl) t (THeads (Flat 
-Appl) t3 (TLRef i))) (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) 
-x3))))))).(\lambda (_: (nf2 c (THeads (Flat Appl) (TCons t1 t3) (TLRef 
-i)))).(\lambda (H15: (eq T (THeads (Flat Appl) (TCons t1 t3) (TLRef i)) 
-(THead (Bind x0) x1 x2))).(let H16 \def (eq_ind T (THead (Flat Appl) t1 
-(THeads (Flat Appl) t3 (TLRef i))) (\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 x0) x1 x2) H15) in (False_ind (eq T (THead (Flat 
-Appl) t (THeads (Flat Appl) (TCons t1 t3) (TLRef i))) (THead (Bind x0) x5 
-(THead (Flat Appl) (lift (S O) O x4) x3))) H16))))))) t0 H_y H9) t2 
-H10))))))))))))) H7)) H6))))))) H2)))))) vs)))).
-(* COMMENTS
-Initial nodes: 2915
-END *)
+ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ 
+_ _) \Rightarrow False])) I (THead (Bind x0) x1 x2) H15) in (False_ind (eq T 
+(THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))) (THead (Bind x0) x5 
+(THead (Flat Appl) (lift (S O) O x4) x3))) H16)))) (\lambda (t1: T).(\lambda 
+(t3: TList).(\lambda (_: (((nf2 c (THeads (Flat Appl) t3 (TLRef i))) \to ((eq 
+T (THeads (Flat Appl) t3 (TLRef i)) (THead (Bind x0) x1 x2)) \to (eq T (THead 
+(Flat Appl) t (THeads (Flat Appl) t3 (TLRef i))) (THead (Bind x0) x5 (THead 
+(Flat Appl) (lift (S O) O x4) x3))))))).(\lambda (_: (nf2 c (THeads (Flat 
+Appl) (TCons t1 t3) (TLRef i)))).(\lambda (H15: (eq T (THeads (Flat Appl) 
+(TCons t1 t3) (TLRef i)) (THead (Bind x0) x1 x2))).(let H16 \def (eq_ind T 
+(THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i))) (\lambda (ee: 
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
+| (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat 
+_) \Rightarrow True])])) I (THead (Bind x0) x1 x2) H15) in (False_ind (eq T 
+(THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t3) (TLRef i))) (THead 
+(Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))) H16))))))) t0 H_y H9) 
+t2 H10))))))))))))) H7)) H6))))))) H2)))))) vs)))).
 
 theorem nf2_appl_lref:
  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (i: nat).((nf2 c 
@@ -283,11 +262,8 @@ theorem nf2_appl_lref:
  \lambda (c: C).(\lambda (u: T).(\lambda (H: (nf2 c u)).(\lambda (i: 
 nat).(\lambda (H0: (nf2 c (TLRef i))).(let H_y \def (nf2_appls_lref c i H0 
 (TCons u TNil)) in (H_y (conj (nf2 c u) True H I))))))).
-(* COMMENTS
-Initial nodes: 49
-END *)
 
-theorem nf2_lref_abst:
+lemma nf2_lref_abst:
  \forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (i: nat).((getl i c 
 (CHead e (Bind Abst) u)) \to (nf2 c (TLRef i))))))
 \def
@@ -308,19 +284,14 @@ O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T (TLRef i) t))
 (let H5 \def (eq_ind C (CHead e (Bind Abst) u) (\lambda (c0: C).(getl i c 
 c0)) H (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead e (Bind Abst) u) i H 
 (CHead x0 (Bind Abbr) x1) H3)) in (let H6 \def (eq_ind C (CHead e (Bind Abst) 
-u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort 
-_) \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return 
-(\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return 
-(\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow True | 
-Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead x0 (Bind 
-Abbr) x1) (getl_mono c (CHead e (Bind Abst) u) i H (CHead x0 (Bind Abbr) x1) 
-H3)) in (False_ind (eq T (TLRef i) (lift (S i) O x1)) H6))) t2 H4))))) H2)) 
-H1)))))))).
-(* COMMENTS
-Initial nodes: 494
-END *)
+u) (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k 
+_) \Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr 
+\Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat 
+_) \Rightarrow False])])) I (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead e 
+(Bind Abst) u) i H (CHead x0 (Bind Abbr) x1) H3)) in (False_ind (eq T (TLRef 
+i) (lift (S i) O x1)) H6))) t2 H4))))) H2)) H1)))))))).
 
-theorem nf2_lift:
+lemma nf2_lift:
  \forall (d: C).(\forall (t: T).((nf2 d t) \to (\forall (c: C).(\forall (h: 
 nat).(\forall (i: nat).((drop h i c d) \to (nf2 c (lift h i t))))))))
 \def
@@ -335,7 +306,4 @@ T (lift h i t) t0)) (let H_y \def (H x H4) in (let H5 \def (eq_ind_r T x
 (\lambda (t0: T).(pr2 d t t0)) H4 t H_y) in (eq_ind T t (\lambda (t0: T).(eq 
 T (lift h i t) (lift h i t0))) (refl_equal T (lift h i t)) x H_y))) t2 H3)))) 
 H2)))))))))).
-(* COMMENTS
-Initial nodes: 245
-END *)