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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/clear/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/clear/drop.ma
index 5dcff6de4..aae3fedc0 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/clear/drop.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/clear/drop.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/clear/fwd.ma".
+include "Basic-1/clear/fwd.ma".
 
-include "LambdaDelta-1/drop/fwd.ma".
+include "Basic-1/drop/fwd.ma".
 
 theorem drop_clear:
  \forall (c1: C).(\forall (c2: C).(\forall (i: nat).((drop (S i) O c1 c2) \to 
@@ -62,6 +62,9 @@ C).(\lambda (_: T).(drop i O e c2)))) (ex2_3 B C T (\lambda (b: B).(\lambda
 (Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e 
 c2)))) x0 x1 x2 (clear_flat c (CHead x1 (Bind x0) x2) H3 f t) H4)))))) H2)))) 
 k (drop_gen_drop k c c2 t i H0))))))))) c1).
+(* COMMENTS
+Initial nodes: 770
+END *)
 
 theorem drop_clear_O:
  \forall (b: B).(\forall (c: C).(\forall (e1: C).(\forall (u: T).((clear c 
@@ -100,6 +103,9 @@ H7) in (eq_ind B b (\lambda (b1: B).(drop (S i) O (CHead c0 (Bind b1) t) e2))
 F).(\lambda (H2: (clear (CHead c0 (Flat f) t) (CHead e1 (Bind b) 
 u))).(drop_drop (Flat f) i c0 e2 (H e1 u (clear_gen_flat f c0 (CHead e1 (Bind 
 b) u) t H2) e2 i H1) t))) k H0))))))))))) c)).
+(* COMMENTS
+Initial nodes: 619
+END *)
 
 theorem drop_clear_S:
  \forall (x2: C).(\forall (x1: C).(\forall (h: nat).(\forall (d: nat).((drop 
@@ -169,4 +175,7 @@ u)))).(\lambda (H8: (drop h d x0 c2)).(ex_intro2 C (\lambda (c1: C).(clear
 u)))) (\lambda (c1: C).(drop h d c1 c2)) x0 (clear_flat x (CHead x0 (Bind b) 
 (lift h d u)) H7 f (lift h (r (Flat f) d) t)) H8)))) H6))))) k H1 H3) x1 
 H2)))) (drop_gen_skip_r c x1 t h d k H0)))))))))))))) x2).
+(* COMMENTS
+Initial nodes: 1449
+END *)