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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubv/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubv/getl.ma
index f78859458..bbba95084 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubv/getl.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubv/getl.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubv/clear.ma".
+include "Basic-1/csubv/clear.ma".
 
-include "LambdaDelta-1/csubv/drop.ma".
+include "Basic-1/csubv/drop.ma".
 
-include "LambdaDelta-1/getl/fwd.ma".
+include "Basic-1/getl/fwd.ma".
 
 theorem csubv_getl_conf:
  \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1: 
@@ -52,6 +52,9 @@ B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))))
 (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind 
 b2) v2))))) x1 x2 x3 H8 (getl_intro i c2 (CHead x2 (Bind x1) x3) x0 H6 
 H9))))))) H7)))))) H4)))))) H1))))))))).
+(* COMMENTS
+Initial nodes: 455
+END *)
 
 theorem csubv_getl_conf_void:
  \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (d1: 
@@ -81,4 +84,7 @@ x1)).(\lambda (H9: (clear x0 (CHead x1 (Bind Void) x2))).(ex2_2_intro C T
 (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda 
 (v2: T).(getl i c2 (CHead d2 (Bind Void) v2)))) x1 x2 H8 (getl_intro i c2 
 (CHead x1 (Bind Void) x2) x0 H6 H9)))))) H7)))))) H4)))))) H1)))))))).
+(* COMMENTS
+Initial nodes: 417
+END *)