X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fcsubt%2Fgetl.ma;h=df14528edec30de955bf0cb29dce3613c37e2a8c;hb=d3c72253769956a8af10e6ea990ed34c92999e58;hp=fc4f15e7ebcd51f3ed266315b50c91c2c2cb3327;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

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 fc4f15e7e..df14528ed 100644
--- 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 *)