X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fcsuba%2Fdrop.ma;h=1047ac13dee1b86e5fed395b607fe0d4528592ce;hb=d6a9ed2a08fcc4e3e26a40cde8cab88c2c69cb3a;hp=6b30e0e1b69615bd3b7ac2261201e5ed140be9cd;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/drop.ma
index 6b30e0e1b..1047ac13d 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/drop.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/drop.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csuba/fwd.ma".
+include "Basic-1/csuba/fwd.ma".
 
-include "LambdaDelta-1/drop/fwd.ma".
+include "Basic-1/drop/fwd.ma".
 
 theorem csuba_drop_abbr:
  \forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).((drop i 
@@ -184,6 +184,9 @@ O (CHead x0 (Flat f) x1) (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g
 d1 d2)) x (drop_drop (Flat f) n x0 (CHead x (Bind Abbr) u) H9 x1) H10)))) 
 H8)) c2 H6))))) H5)))))) k H2 (drop_gen_drop k c (CHead d1 (Bind Abbr) u) t n 
 H1)))))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 3648
+END *)
 
 theorem csuba_drop_abst:
  \forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i 
@@ -799,6 +802,9 @@ g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
 A).(arity g d2 u2 a)))) x2 x3 x4 (drop_drop (Flat f) n x0 (CHead x2 (Bind 
 Abbr) x3) H10 x1) H11 H12 H13))))))))) H9)) H8)) c2 H6))))) H5)))))) k H2 
 (drop_gen_drop k c (CHead d1 (Bind Abst) u1) t n H1)))))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 12528
+END *)
 
 theorem csuba_drop_abst_rev:
  \forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).((drop i 
@@ -1306,6 +1312,9 @@ Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1))) x2 x3
 (drop_drop (Flat f) n x0 (CHead x2 (Bind Void) x3) H10 x1) H11)))))) H9)) 
 H8)) c2 H6))))) H5)))))) k H2 (drop_gen_drop k c (CHead d1 (Bind Abst) u) t n 
 H1)))))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 11438
+END *)
 
 theorem csuba_drop_abbr_rev:
  \forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i 
@@ -2453,4 +2462,7 @@ T).(drop (S n) O (CHead x0 (Flat f) x1) (CHead d2 (Bind Void) u2)))) (\lambda
 (d2: C).(\lambda (_: T).(csuba g d2 d1))) x2 x3 (drop_drop (Flat f) n x0 
 (CHead x2 (Bind Void) x3) H10 x1) H11)))))) H9)) H8)) c2 H6))))) H5)))))) k 
 H2 (drop_gen_drop k c (CHead d1 (Bind Abbr) u1) t n H1)))))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 23852
+END *)