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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/getl.ma
index 8b7cab309..b49d9b7c2 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/getl.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/getl.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csuba/drop.ma".
+include "Basic-1/csuba/drop.ma".
 
-include "LambdaDelta-1/csuba/clear.ma".
+include "Basic-1/csuba/clear.ma".
 
-include "LambdaDelta-1/getl/clear.ma".
+include "Basic-1/getl/clear.ma".
 
 theorem csuba_getl_abbr:
  \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall 
@@ -135,6 +135,9 @@ x9)).(ex_intro2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind Abbr) u)))
 (\lambda (d2: C).(csuba g d1 d2)) x9 (getl_clear_bind x6 c2 x7 x8 H20 (CHead 
 x9 (Bind Abbr) u) n H22) H23)))) H21)))))))) H17)))))) H14))))))) H11)))))))) 
 i) H7))))) k H3 H4))))))) x H1 H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 2319
+END *)
 
 theorem csuba_getl_abst:
  \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).(\forall 
@@ -470,6 +473,9 @@ T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
 c2 x7 x8 H20 (CHead x9 (Bind Abbr) x10) n H23) H24 H25 H26))))))))) H22)) 
 H21)))))))) H17)))))) H14))))))) H11)))))))) i) H7))))) k H3 H4))))))) x H1 
 H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 6437
+END *)
 
 theorem csuba_getl_abst_rev:
  \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall 
@@ -698,6 +704,9 @@ d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(getl (S n) c2 (CHead d2
 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Void) x10) n H23) H24)))))) 
 H22)) H21)))))))) H17)))))) H14))))))) H11)))))))) i) H7))))) k H3 H4))))))) 
 x H1 H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 4703
+END *)
 
 theorem csuba_getl_abbr_rev:
  \forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).(\forall 
@@ -1163,4 +1172,7 @@ u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) x9 x10
 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Void) x10) n H23) H24)))))) 
 H22)) H21)))))))) H17)))))) H14))))))) H11)))))))) i) H7))))) k H3 H4))))))) 
 x H1 H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 9091
+END *)