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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/drop.ma
index d34cd09a1..adaedcc9a 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/drop.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/drop.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubt/fwd.ma".
+include "Basic-1/csubt/fwd.ma".
 
-include "LambdaDelta-1/drop/fwd.ma".
+include "Basic-1/drop/fwd.ma".
 
 theorem csubt_drop_flat:
  \forall (g: G).(\forall (f: F).(\forall (n: nat).(\forall (c1: C).(\forall 
@@ -115,6 +115,9 @@ c3 (CHead x (Flat f) u0))).(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2))
 u0))) x H6 (drop_drop (Bind Abbr) n0 c3 (CHead x (Flat f) u0) H7 u))))) (H c0 
 c3 H1 d1 u0 (drop_gen_drop (Bind Abst) c0 (CHead d1 (Flat f) u0) t n0 
 H5)))))))))))))) c1 c2 H0)))))) n))).
+(* COMMENTS
+Initial nodes: 2090
+END *)
 
 theorem csubt_drop_abbr:
  \forall (g: G).(\forall (n: nat).(\forall (c1: C).(\forall (c2: C).((csubt g 
@@ -215,6 +218,9 @@ C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CHead c3 (Bind Abbr) u)
 (CHead d2 (Bind Abbr) u0))) x H6 (drop_drop (Bind Abbr) n0 c3 (CHead x (Bind 
 Abbr) u0) H7 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop (Bind Abst) c0 (CHead d1 
 (Bind Abbr) u0) t n0 H5)))))))))))))) c1 c2 H0)))))) n)).
+(* COMMENTS
+Initial nodes: 2084
+END *)
 
 theorem csubt_drop_abst:
  \forall (g: G).(\forall (n: nat).(\forall (c1: C).(\forall (c2: C).((csubt g 
@@ -578,4 +584,7 @@ C).(\lambda (u0: T).(ty3 g d1 u0 t0))) (\lambda (d2: C).(\lambda (u0: T).(ty3
 g d2 u0 t0))) x0 x1 H7 (drop_drop (Bind Abbr) n0 c3 (CHead x0 (Bind Abbr) x1) 
 H8 u) H9 H10)))))))) H6)) (H c0 c3 H1 d1 t0 (drop_gen_drop (Bind Abst) c0 
 (CHead d1 (Bind Abst) t0) t n0 H5)))))))))))))) c1 c2 H0)))))) n)).
+(* COMMENTS
+Initial nodes: 7940
+END *)