X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fty3%2Ffwd.ma;h=bf6634e451e6e3b7b78acab46041119e3ec42adf;hb=d6a9ed2a08fcc4e3e26a40cde8cab88c2c69cb3a;hp=69f001666f7a3f6517f832bbb592dcadd14f3e4f;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fwd.ma
index 69f001666..bf6634e45 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/fwd.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/ty3/defs.ma".
+include "Basic-1/ty3/defs.ma".
 
-include "LambdaDelta-1/pc3/props.ma".
+include "Basic-1/pc3/props.ma".
 
 theorem ty3_gen_sort:
  \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((ty3 g c 
@@ -85,6 +85,9 @@ ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) 
 H5) in (False_ind (pc3 c0 (TSort (next g n)) (THead (Flat Cast) t0 t2)) 
 H6))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 1179
+END *)
 
 theorem ty3_gen_lref:
  \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((ty3 g c 
@@ -378,6 +381,9 @@ T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda
 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind 
 Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u 
 t)))))) H6))))))))))) c y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 5569
+END *)
 
 theorem ty3_gen_bind:
  \forall (g: G).(\forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t1: 
@@ -551,6 +557,9 @@ t0) (THead (Bind b) u t1))).(let H6 \def (eq_ind T (THead (Flat Cast) t2 t0)
 (THead (Flat Cast) t3 t2)))) (\lambda (_: T).(\lambda (t: T).(ty3 g c0 u t))) 
 (\lambda (t4: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u) t1 t4)))) 
 H6))))))))))) c y x H0))) H))))))).
+(* COMMENTS
+Initial nodes: 3389
+END *)
 
 theorem ty3_gen_appl:
  \forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (v: T).(\forall (x: 
@@ -716,6 +725,9 @@ True])])])) I (THead (Flat Appl) w v) H5) in (False_ind (ex3_2 T T (\lambda
 (THead (Flat Cast) t0 t2)))) (\lambda (u: T).(\lambda (t: T).(ty3 g c0 v 
 (THead (Bind Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c0 w u)))) 
 H6))))))))))) c y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 3171
+END *)
 
 theorem ty3_gen_cast:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).(\forall 
@@ -848,6 +860,9 @@ c0 t t2)) H12 t1 H7) in (ex3_intro T (\lambda (t5: T).(pc3 c0 (THead (Flat
 Cast) t5 t2) (THead (Flat Cast) t4 t2))) (\lambda (_: T).(ty3 g c0 t1 t2)) 
 (\lambda (t5: T).(ty3 g c0 t2 t5)) t4 (pc3_refl c0 (THead (Flat Cast) t4 t2)) 
 H14 H10))) t3 H8))))))) H6))))))))))) c y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 2609
+END *)
 
 theorem tys3_gen_nil:
  \forall (g: G).(\forall (c: C).(\forall (u: T).((tys3 g c TNil u) \to (ex T 
@@ -867,6 +882,9 @@ ts) TNil)).(let H5 \def (eq_ind TList (TCons t ts) (\lambda (ee:
 TList).(match ee in TList return (\lambda (_: TList).Prop) with [TNil 
 \Rightarrow False | (TCons _ _) \Rightarrow True])) I TNil H4) in (False_ind 
 (ex T (\lambda (u1: T).(ty3 g c u0 u1))) H5))))))))) y u H0))) H)))).
+(* COMMENTS
+Initial nodes: 255
+END *)
 
 theorem tys3_gen_cons:
  \forall (g: G).(\forall (c: C).(\forall (ts: TList).(\forall (t: T).(\forall 
@@ -898,4 +916,7 @@ TList).TList) with [TNil \Rightarrow ts0 | (TCons _ t1) \Rightarrow t1]))
 ts0 (\lambda (t1: TList).(tys3 g c t1 u0)) H2 ts H6) in (let H10 \def (eq_ind 
 T t0 (\lambda (t1: T).(ty3 g c t1 u0)) H1 t H7) in (conj (ty3 g c t u0) (tys3 
 g c ts u0) H10 H9)))))) H5))))))))) y u H0))) H)))))).
+(* COMMENTS
+Initial nodes: 479
+END *)