X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fwf3%2Fprops.ma;h=98a05c6378bbd46baa2bc1906d30b1148886dd09;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=8fb22a1dc25a6e1981de0d6cd5ec232c677b977d;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/props.ma
index 8fb22a1dc..98a05c637 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/wf3/ty3.ma".
+include "Basic-1/wf3/ty3.ma".
 
-include "LambdaDelta-1/app/defs.ma".
+include "Basic-1/app/defs.ma".
 
 theorem wf3_mono:
  \forall (g: G).(\forall (c: C).(\forall (c1: C).((wf3 g c c1) \to (\forall 
@@ -94,6 +94,9 @@ c3 x0 (Bind Void) (Bind Void) (TSort O) (TSort O) (H1 x0 H7) (refl_equal K
 T).(\lambda (f: F).(\lambda (c0: C).(\lambda (H2: (wf3 g (CHead c2 (Flat f) 
 u) c0)).(let H_y \def (wf3_gen_flat1 g c2 c0 u f H2) in (H1 c0 H_y)))))))))) 
 c c1 H)))).
+(* COMMENTS
+Initial nodes: 1555
+END *)
 
 theorem wf3_total:
  \forall (g: G).(\forall (c1: C).(ex C (\lambda (c2: C).(wf3 g c1 c2))))
@@ -117,6 +120,9 @@ False)))).(ex_intro C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2))
 (CHead x (Bind Void) (TSort O)) (wf3_void g c x H1 t H3 b))) H2)))) (\lambda 
 (f: F).(ex_intro C (\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2)) x 
 (wf3_flat g c x H1 t f))) k))) H0)))))) c1)).
+(* COMMENTS
+Initial nodes: 435
+END *)
 
 theorem ty3_shift1:
  \forall (g: G).(\forall (c: C).((wf3 g c c) \to (\forall (t1: T).(\forall 
@@ -202,6 +208,9 @@ K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])) I
 (Bind x) H9) in (False_ind (ty3 g (CSort (cbk c1)) (app1 c1 (THead (Flat f) u 
 t1)) (app1 c1 (THead (Flat f) u t2))) H10)))) H8)))))))))))))))) y c H0))) 
 H))).
+(* COMMENTS
+Initial nodes: 1677
+END *)
 
 theorem wf3_idem:
  \forall (g: G).(\forall (c1: C).(\forall (c2: C).((wf3 g c1 c2) \to (wf3 g 
@@ -218,6 +227,9 @@ c3 u t H2 c4 H0) b))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (_:
 c4 H1 (TSort O) (TSort (next g O)) (ty3_sort g c4 O) Void)))))))) (\lambda 
 (c3: C).(\lambda (c4: C).(\lambda (_: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4 
 c4)).(\lambda (_: T).(\lambda (_: F).H1)))))) c1 c2 H)))).
+(* COMMENTS
+Initial nodes: 207
+END *)
 
 theorem wf3_ty3:
  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (u: T).((ty3 g c1 t 
@@ -230,4 +242,7 @@ C (\lambda (c2: C).(wf3 g c1 c2)) (ex2 C (\lambda (c2: C).(wf3 g c1 c2))
 (\lambda (c2: C).(ty3 g c2 t u))) (\lambda (x: C).(\lambda (H1: (wf3 g c1 
 x)).(ex_intro2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(ty3 g c2 t 
 u)) x H1 (wf3_ty3_conf g c1 t u H x H1)))) H0))))))).
+(* COMMENTS
+Initial nodes: 123
+END *)