X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fwf3%2Fclear.ma;h=b2ddd47af9c12718e6d86eab6ca6aaec2bb8c36c;hb=964844c87f7c3d7061dfeb7f2d84b6b8bbcdaf13;hp=ead56e7a74403c425288ed6bd850d15b368c00ad;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/clear.ma
index ead56e7a7..b2ddd47af 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/clear.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/wf3/clear.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/wf3/fwd.ma".
+include "Basic-1/wf3/fwd.ma".
 
 theorem wf3_clear_conf:
  \forall (c1: C).(\forall (c: C).((clear c1 c) \to (\forall (g: G).(\forall 
@@ -29,6 +29,9 @@ c0)).(\lambda (H1: ((\forall (g: G).(\forall (c2: C).((wf3 g e c2) \to (wf3 g
 c0 c2)))))).(\lambda (f: F).(\lambda (u: T).(\lambda (g: G).(\lambda (c2: 
 C).(\lambda (H2: (wf3 g (CHead e (Flat f) u) c2)).(let H_y \def 
 (wf3_gen_flat1 g e c2 u f H2) in (H1 g c2 H_y))))))))))) c1 c H))).
+(* COMMENTS
+Initial nodes: 145
+END *)
 
 theorem clear_wf3_trans:
  \forall (c1: C).(\forall (d1: C).((clear c1 d1) \to (\forall (g: G).(\forall 
@@ -82,4 +85,7 @@ C).(wf3 g (CHead e (Flat f) u) c2)) (\lambda (c2: C).(clear c2 d2))) (\lambda
 (x: C).(\lambda (H4: (wf3 g e x)).(\lambda (H5: (clear x d2)).(ex_intro2 C 
 (\lambda (c2: C).(wf3 g (CHead e (Flat f) u) c2)) (\lambda (c2: C).(clear c2 
 d2)) x (wf3_flat g e x H4 u f) H5)))) H3)))))))))))) c1 d1 H))).
+(* COMMENTS
+Initial nodes: 1023
+END *)