uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / csubv / clear.ma

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 57e380c5b1b0d941bdc7ccbf1cf1d43f8d994cd3..5c54f5b9ab552b93674cd755f001271bda44bb4b 100644 (file)
--- 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 *)