uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / csubt / getl.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/getl.ma
index fc4f15e7ebcd51f3ed266315b50c91c2c2cb3327..df14528edec30de955bf0cb29dce3613c37e2a8c 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/getl.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/getl.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubt/clear.ma".
+include "Basic-1/csubt/clear.ma".
 
-include "LambdaDelta-1/csubt/drop.ma".
+include "Basic-1/csubt/drop.ma".
 
-include "LambdaDelta-1/getl/clear.ma".
+include "Basic-1/getl/clear.ma".
 
 theorem csubt_getl_abbr:
  \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall 
@@ -135,6 +135,9 @@ d2)) (\lambda (d2: C).(getl (S n0) c2 (CHead d2 (Bind Abbr) u))) x9 H22
 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Abbr) u) n0 H23))))) 
 H21)))))))) H17))))) H14))))))) H11)))))))) n) H7))))) k H3 H4))))))) x H1 
 H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 2313
+END *)
 
 theorem csubt_getl_abst:
  \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (t: T).(\forall 
@@ -417,4 +420,7 @@ x7 (CHead x9 (Bind Abbr) x10))).(\lambda (H25: (ty3 g d1 x10 t)).(\lambda
 g d2 u t))) x9 x10 H23 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Abbr) 
 x10) n0 H24) H25 H26)))))))) H22)) H21)))))))) H17))))) H14))))))) 
 H11)))))))) n) H7))))) k H3 H4))))))) x H1 H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 5861
+END *)