X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fclear%2Fprops.ma;h=68e250d761edb121096de84ccd2ef32a7f35848b;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=134c2144879e5c17889ed0069bd9a43db9dc9eba;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/clear/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/clear/props.ma
index 134c21448..68e250d76 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/clear/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/clear/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/clear/fwd.ma".
+include "Basic-1/clear/fwd.ma".
 
 theorem clear_clear:
  \forall (c1: C).(\forall (c2: C).((clear c1 c2) \to (clear c2 c2)))
@@ -30,6 +30,9 @@ c2)).(eq_ind_r C (CHead c (Bind b) t) (\lambda (c0: C).(clear c0 c0))
 (clear_bind b c t) c2 (clear_gen_bind b c c2 t H1)))) (\lambda (f: 
 F).(\lambda (H1: (clear (CHead c (Flat f) t) c2)).(H c2 (clear_gen_flat f c 
 c2 t H1)))) k H0))))))) c1).
+(* COMMENTS
+Initial nodes: 199
+END *)
 
 theorem clear_mono:
  \forall (c: C).(\forall (c1: C).((clear c c1) \to (\forall (c2: C).((clear c 
@@ -52,6 +55,9 @@ t) c1)).(\lambda (H3: (clear (CHead c0 (Bind b) t) c2)).(eq_ind_r C (CHead c0
 H3))))) (\lambda (f: F).(\lambda (H2: (clear (CHead c0 (Flat f) t) 
 c1)).(\lambda (H3: (clear (CHead c0 (Flat f) t) c2)).(H c1 (clear_gen_flat f 
 c0 c1 t H2) c2 (clear_gen_flat f c0 c2 t H3))))) k H0 H1))))))))) c).
+(* COMMENTS
+Initial nodes: 357
+END *)
 
 theorem clear_trans:
  \forall (c1: C).(\forall (c: C).((clear c1 c) \to (\forall (c2: C).((clear c 
@@ -72,6 +78,9 @@ c0 t H2)) in (eq_ind_r C (CHead c (Bind b) t) (\lambda (c3: C).(clear (CHead
 c (Bind b) t) c3)) (clear_bind b c t) c2 (clear_gen_bind b c c2 t H3))))) 
 (\lambda (f: F).(\lambda (H2: (clear (CHead c (Flat f) t) c0)).(clear_flat c 
 c2 (H c0 (clear_gen_flat f c c0 t H2) c2 H1) f t))) k H0))))))))) c1).
+(* COMMENTS
+Initial nodes: 299
+END *)
 
 theorem clear_ctail:
  \forall (b: B).(\forall (c1: C).(\forall (c2: C).(\forall (u2: T).((clear c1 
@@ -117,6 +126,9 @@ k0 u1 c) t) b0 H5) c2 H6) u2 H4)))) H3)) H2)))) (\lambda (f: F).(\lambda (H1:
 (clear (CHead c (Flat f) t) (CHead c2 (Bind b) u2))).(clear_flat (CTail k0 u1 
 c) (CHead (CTail k0 u1 c2) (Bind b) u2) (H c2 u2 (clear_gen_flat f c (CHead 
 c2 (Bind b) u2) t H1) k0 u1) f t))) k H0)))))))))) c1)).
+(* COMMENTS
+Initial nodes: 819
+END *)
 
 theorem clear_cle:
  \forall (c1: C).(\forall (c2: C).((clear c1 c2) \to (cle c2 c1)))
@@ -134,4 +146,7 @@ C).(\lambda (H0: (clear (CHead c k t) c2)).(K_ind (\lambda (k0: K).((clear
 c2 t H1)))) (\lambda (f: F).(\lambda (H1: (clear (CHead c (Flat f) t) 
 c2)).(le_plus_trans (cweight c2) (cweight c) (tweight t) (H c2 
 (clear_gen_flat f c c2 t H1))))) k H0))))))) c1).
+(* COMMENTS
+Initial nodes: 247
+END *)