X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fcsubv%2Fclear.ma;h=5c54f5b9ab552b93674cd755f001271bda44bb4b;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=57e380c5b1b0d941bdc7ccbf1cf1d43f8d994cd3;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubv/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubv/clear.ma
index 57e380c5b..5c54f5b9a 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubv/clear.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubv/clear.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubv/defs.ma".
+include "Basic-1/csubv/defs.ma".
 
-include "LambdaDelta-1/clear/fwd.ma".
+include "Basic-1/clear/fwd.ma".
 
 theorem csubv_clear_conf:
  \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1: 
@@ -107,6 +107,9 @@ C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
 C).(\lambda (v3: T).(clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind b2) 
 v3))))) x0 x1 x2 H4 (clear_flat c4 (CHead x1 (Bind x0) x2) H5 f2 v2))))))) 
 H3))))))))))))))) c1 c2 H))).
+(* COMMENTS
+Initial nodes: 1357
+END *)
 
 theorem csubv_clear_conf_void:
  \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (d1: 
@@ -185,4 +188,7 @@ d1 x0)).(\lambda (H5: (clear c4 (CHead x0 (Bind Void) x1))).(ex2_2_intro C T
 (v3: T).(clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3)))) x0 x1 H4 
 (clear_flat c4 (CHead x0 (Bind Void) x1) H5 f2 v2)))))) H3)))))))))))))) c1 
 c2 H))).
+(* COMMENTS
+Initial nodes: 1205
+END *)