X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fty3%2Fnf2.ma;h=e9cf818b747236cac12477489e9939fd745eaa46;hb=639e798161afea770f41d78673c0fe3be4125beb;hp=47b675663abb30e2bbe04bcca816d2431ed552f0;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/ty3/nf2.ma b/matita/matita/contribs/lambdadelta/basic_1/ty3/nf2.ma
index 47b675663..e9cf818b7 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/ty3/nf2.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/ty3/nf2.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/ty3/arity.ma".
+include "basic_1/ty3/arity.ma".
 
-include "Basic-1/pc3/nf2.ma".
+include "basic_1/pc3/nf2.ma".
 
-include "Basic-1/nf2/arity.ma".
+include "basic_1/nf2/arity.ma".
 
 definition ty3_nf2_inv_abst_premise:
  C \to (T \to (T \to Prop))
@@ -37,9 +37,6 @@ theorem ty3_nf2_inv_abst_premise_csort:
 wi))).(\lambda (vs: TList).(\lambda (_: (pc3 (CSort m) (THeads (Flat Appl) vs 
 (lift (S i) O wi)) (THead (Bind Abst) w u))).(getl_gen_sort m i (CHead d 
 (Bind Abst) wi) H False))))))))).
-(* COMMENTS
-Initial nodes: 85
-END *)
 
 theorem ty3_nf2_inv_all:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t 
@@ -63,9 +60,6 @@ i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
 TList).(\lambda (i: nat).(nf2 c (TLRef i)))))) (\lambda (x: A).(\lambda (H2: 
 (arity g c t x)).(\lambda (_: (arity g c u (asucc g x))).(arity_nf2_inv_all g 
 c t x H2 H0)))) H1)))))))).
-(* COMMENTS
-Initial nodes: 233
-END *)
 
 theorem ty3_nf2_inv_sort:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (m: nat).((ty3 g c t 
@@ -178,9 +172,6 @@ x1)) (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
 nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef i)))) 
 x0 x1 (refl_equal T (THeads (Flat Appl) x0 (TLRef x1))) H4 H5)) t H3))))))) 
 H2)) H1)))))))).
-(* COMMENTS
-Initial nodes: 2045
-END *)
 
 theorem ty3_nf2_gen__ty3_nf2_inv_abst_aux:
  \forall (c: C).(\forall (w1: T).(\forall (u1: T).((ty3_nf2_inv_abst_premise 
@@ -201,9 +192,6 @@ wi))).(\lambda (vs: TList).(\lambda (H2: (pc3 c (THeads (Flat Appl) vs (lift
 (THeads (Flat Appl) vs (lift (S i) O wi))) (pc3_thin_dx c (THeads (Flat Appl) 
 vs (lift (S i) O wi)) (THead (Bind Abst) w2 u2) H2 t Appl) (THead (Bind Abst) 
 w1 u1) H0))))))))))))))).
-(* COMMENTS
-Initial nodes: 271
-END *)
 
 theorem ty3_nf2_inv_abst:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (w: T).(\forall (u: 
@@ -439,34 +427,29 @@ Appl) t2 (TLRef x1))) (THead (Bind Abst) x v)))) (\lambda (_: T).(\lambda
 (Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind 
 Abst) x) v)))))) (\lambda (H22: (eq T (THeads (Flat Appl) TNil (TLRef x1)) 
 (THead (Bind Abst) x3 x5))).(let H23 \def (eq_ind T (TLRef x1) (\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) x3 x5) H22) in (False_ind (ex4_2 T T (\lambda (v: 
-T).(\lambda (_: T).(eq T (THead (Flat Appl) t0 (THeads (Flat Appl) TNil 
-(TLRef x1))) (THead (Bind Abst) x v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 
-g c x w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) x) v 
-x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) x) v)))) 
-H23))) (\lambda (t2: T).(\lambda (t3: TList).(\lambda (_: (((eq T (THeads 
-(Flat Appl) t3 (TLRef x1)) (THead (Bind Abst) x3 x5)) \to (ex4_2 T T (\lambda 
-(v: T).(\lambda (_: T).(eq T (THead (Flat Appl) t0 (THeads (Flat Appl) t3 
-(TLRef x1))) (THead (Bind Abst) x v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 
-g c x w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) x) v 
-x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) x) 
-v))))))).(\lambda (H22: (eq T (THeads (Flat Appl) (TCons t2 t3) (TLRef x1)) 
-(THead (Bind Abst) x3 x5))).(let H23 \def (eq_ind T (THead (Flat Appl) t2 
-(THeads (Flat Appl) t3 (TLRef x1))) (\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) x3 x5) H22) in (False_ind (ex4_2 T T (\lambda 
-(v: T).(\lambda (_: T).(eq T (THead (Flat Appl) t0 (THeads (Flat Appl) (TCons 
-t2 t3) (TLRef x1))) (THead (Bind Abst) x v)))) (\lambda (_: T).(\lambda (w0: 
-T).(ty3 g c x w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind 
-Abst) x) v x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) x) 
-v)))) H23)))))) t1 H18))))))) H17))))))))) (ty3_gen_appl g c t0 (THeads (Flat 
-Appl) t1 (TLRef x1)) (THead (Bind Abst) x x2) H12))))))))) x0)) H10)) H9)) t 
-H5))))))) H4)) H3))))))))))).
-(* COMMENTS
-Initial nodes: 5333
-END *)
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
+(THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) x3 x5) H22) in 
+(False_ind (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead (Flat 
+Appl) t0 (THeads (Flat Appl) TNil (TLRef x1))) (THead (Bind Abst) x v)))) 
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) (\lambda (v: T).(\lambda 
+(_: T).(ty3 g (CHead c (Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_: 
+T).(nf2 (CHead c (Bind Abst) x) v)))) H23))) (\lambda (t2: T).(\lambda (t3: 
+TList).(\lambda (_: (((eq T (THeads (Flat Appl) t3 (TLRef x1)) (THead (Bind 
+Abst) x3 x5)) \to (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead 
+(Flat Appl) t0 (THeads (Flat Appl) t3 (TLRef x1))) (THead (Bind Abst) x v)))) 
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) (\lambda (v: T).(\lambda 
+(_: T).(ty3 g (CHead c (Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_: 
+T).(nf2 (CHead c (Bind Abst) x) v))))))).(\lambda (H22: (eq T (THeads (Flat 
+Appl) (TCons t2 t3) (TLRef x1)) (THead (Bind Abst) x3 x5))).(let H23 \def 
+(eq_ind T (THead (Flat Appl) t2 (THeads (Flat Appl) t3 (TLRef x1))) (\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) x3 x5) H22) in (False_ind 
+(ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead (Flat Appl) t0 
+(THeads (Flat Appl) (TCons t2 t3) (TLRef x1))) (THead (Bind Abst) x v)))) 
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) (\lambda (v: T).(\lambda 
+(_: T).(ty3 g (CHead c (Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_: 
+T).(nf2 (CHead c (Bind Abst) x) v)))) H23)))))) t1 H18))))))) H17))))))))) 
+(ty3_gen_appl g c t0 (THeads (Flat Appl) t1 (TLRef x1)) (THead (Bind Abst) x 
+x2) H12))))))))) x0)) H10)) H9)) t H5))))))) H4)) H3))))))))))).