X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fnf2%2Fdec.ma;h=d7211841f02e9ead56cdd76d9649e3a484764165;hp=33b652bafa8dce7632b4bfe91a51acd884c1c3a7;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hpb=88a68a9c334646bc17314d5327cd3b790202acd6

diff --git a/matita/matita/contribs/lambdadelta/basic_1/nf2/dec.ma b/matita/matita/contribs/lambdadelta/basic_1/nf2/dec.ma
index 33b652baf..d7211841f 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/nf2/dec.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/nf2/dec.ma
@@ -14,17 +14,15 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/nf2/defs.ma".
+include "basic_1/nf2/defs.ma".
 
-include "Basic-1/pr2/clen.ma".
+include "basic_1/pr2/clen.ma".
 
-include "Basic-1/pr2/fwd.ma".
+include "basic_1/pr0/dec.ma".
 
-include "Basic-1/pr0/dec.ma".
+include "basic_1/C/props.ma".
 
-include "Basic-1/C/props.ma".
-
-theorem nf2_dec:
+lemma nf2_dec:
  \forall (c: C).(\forall (t1: T).(or (nf2 c t1) (ex2 T (\lambda (t2: T).((eq 
 T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c t1 t2)))))
 \def
@@ -144,14 +142,13 @@ K (Bind Abst) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0:
 T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5: 
 (eq K (Bind Abst) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_: 
 (subst0 (clen c0) t x0 t2)).(let H8 \def (eq_ind K (Bind Abst) (\lambda (ee: 
-K).(match ee in K return (\lambda (_: K).Prop) with [(Bind b0) \Rightarrow 
-(match b0 in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | 
-Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _) \Rightarrow 
-False])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3)))))) 
-(or_introl (\forall (t2: T).((pr2 (CTail (Bind Void) t c0) t1 t2) \to (eq T 
-t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) 
-(\lambda (t2: T).(pr2 (CTail (Bind Void) t c0) t1 t2))) (\lambda (t2: 
-T).(\lambda (H2: (pr2 (CTail (Bind Void) t c0) t1 t2)).(let H_x0 \def 
+K).(match ee with [(Bind b0) \Rightarrow (match b0 with [Abbr \Rightarrow 
+False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _) 
+\Rightarrow False])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) 
+H4)) H3)))))) (or_introl (\forall (t2: T).((pr2 (CTail (Bind Void) t c0) t1 
+t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: 
+Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Void) t c0) t1 t2))) (\lambda 
+(t2: T).(\lambda (H2: (pr2 (CTail (Bind Void) t c0) t1 t2)).(let H_x0 \def 
 (pr2_gen_ctail (Bind Void) c0 t t1 t2 H2) in (let H3 \def H_x0 in (or_ind 
 (pr2 c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Bind Void) (Bind Abbr))) 
 (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2))) 
@@ -162,39 +159,35 @@ K (Bind Void) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0:
 T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5: 
 (eq K (Bind Void) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_: 
 (subst0 (clen c0) t x0 t2)).(let H8 \def (eq_ind K (Bind Void) (\lambda (ee: 
-K).(match ee in K return (\lambda (_: K).Prop) with [(Bind b0) \Rightarrow 
-(match b0 in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | 
-Abst \Rightarrow False | Void \Rightarrow True]) | (Flat _) \Rightarrow 
-False])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3)))))) 
-b)) (\lambda (f: F).(or_introl (\forall (t2: T).((pr2 (CTail (Flat f) t c0) 
-t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall 
-(P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Flat f) t c0) t1 t2))) (\lambda 
-(t2: T).(\lambda (H2: (pr2 (CTail (Flat f) t c0) t1 t2)).(let H_x0 \def 
-(pr2_gen_ctail (Flat f) c0 t t1 t2 H2) in (let H3 \def H_x0 in (or_ind (pr2 
-c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Flat f) (Bind Abbr))) (\lambda (t0: 
-T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2))) (eq T t1 t2) 
-(\lambda (H4: (pr2 c0 t1 t2)).(H1 t2 H4)) (\lambda (H4: (ex3 T (\lambda (_: 
+K).(match ee with [(Bind b0) \Rightarrow (match b0 with [Abbr \Rightarrow 
+False | Abst \Rightarrow False | Void \Rightarrow True]) | (Flat _) 
+\Rightarrow False])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) 
+H4)) H3)))))) b)) (\lambda (f: F).(or_introl (\forall (t2: T).((pr2 (CTail 
+(Flat f) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 
+t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Flat f) t c0) 
+t1 t2))) (\lambda (t2: T).(\lambda (H2: (pr2 (CTail (Flat f) t c0) t1 
+t2)).(let H_x0 \def (pr2_gen_ctail (Flat f) c0 t t1 t2 H2) in (let H3 \def 
+H_x0 in (or_ind (pr2 c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Flat f) (Bind 
+Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 
+t2))) (eq T t1 t2) (\lambda (H4: (pr2 c0 t1 t2)).(H1 t2 H4)) (\lambda (H4: 
+(ex3 T (\lambda (_: T).(eq K (Flat f) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 
+t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_: 
 T).(eq K (Flat f) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: 
-T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_: T).(eq K (Flat f) 
-(Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen 
-c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5: (eq K (Flat f) 
-(Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_: (subst0 (clen c0) t x0 
-t2)).(let H8 \def (eq_ind K (Flat f) (\lambda (ee: K).(match ee in K return 
-(\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
-True])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3))))))) 
-k)) (\lambda (H1: (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: 
-Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2)))).(ex2_ind T (\lambda (t2: 
-T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2)) 
-(or (\forall (t2: T).((pr2 (CTail k t c0) t1 t2) \to (eq T t1 t2))) (ex2 T 
-(\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: 
-T).(pr2 (CTail k t c0) t1 t2)))) (\lambda (x: T).(\lambda (H2: (((eq T t1 x) 
-\to (\forall (P: Prop).P)))).(\lambda (H3: (pr2 c0 t1 x)).(or_intror (\forall 
+T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5: 
+(eq K (Flat f) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_: (subst0 
+(clen c0) t x0 t2)).(let H8 \def (eq_ind K (Flat f) (\lambda (ee: K).(match 
+ee with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])) I (Bind 
+Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3))))))) k)) (\lambda 
+(H1: (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) 
+(\lambda (t2: T).(pr2 c0 t1 t2)))).(ex2_ind T (\lambda (t2: T).((eq T t1 t2) 
+\to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2)) (or (\forall 
 (t2: T).((pr2 (CTail k t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: 
 T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail k t 
-c0) t1 t2))) (ex_intro2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: 
-Prop).P))) (\lambda (t2: T).(pr2 (CTail k t c0) t1 t2)) x H2 (pr2_ctail c0 t1 
-x H3 k t)))))) H1)) H0)))))))) c).
-(* COMMENTS
-Initial nodes: 3653
-END *)
+c0) t1 t2)))) (\lambda (x: T).(\lambda (H2: (((eq T t1 x) \to (\forall (P: 
+Prop).P)))).(\lambda (H3: (pr2 c0 t1 x)).(or_intror (\forall (t2: T).((pr2 
+(CTail k t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 
+t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail k t c0) t1 t2))) 
+(ex_intro2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) 
+(\lambda (t2: T).(pr2 (CTail k t c0) t1 t2)) x H2 (pr2_ctail c0 t1 x H3 k 
+t)))))) H1)) H0)))))))) c).