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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/drop.ma
index b18b7c5e6..b6bc6cae7 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/drop.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubst0/drop.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubst0/fwd.ma".
+include "Basic-1/csubst0/fwd.ma".
 
-include "LambdaDelta-1/drop/fwd.ma".
+include "Basic-1/drop/fwd.ma".
 
-include "LambdaDelta-1/s/props.ma".
+include "Basic-1/s/props.ma".
 
 theorem csubst0_drop_gt:
  \forall (n: nat).(\forall (i: nat).((lt i n) \to (\forall (c1: C).(\forall 
@@ -161,6 +161,9 @@ nat).(\lambda (_: (eq nat x2 (S x))).(\lambda (_: (lt x n0)).(drop_drop (Flat
 f) n0 x1 e (H12 x1 v H8 e H11) x0)))) H14)) (lt_gen_xS x2 n0 H13)))))) k 
 (drop_gen_drop k c e t n0 H3) H9 H10))) c2 H6)))))))) H4)) (csubst0_gen_head 
 k c c2 t v i H2))))))))))) c1)))))) n).
+(* COMMENTS
+Initial nodes: 3092
+END *)
 
 theorem csubst0_drop_gt_back:
  \forall (n: nat).(\forall (i: nat).((lt i n) \to (\forall (c1: C).(\forall 
@@ -297,6 +300,9 @@ nat).(eq nat x2 (S m))) (\lambda (m: nat).(lt m n0)))).(ex2_ind nat (\lambda
 x))).(\lambda (_: (lt x n0)).(drop_drop (Flat f) n0 c e (H12 x1 v H8 e H14) 
 t)))) H15)) (lt_gen_xS x2 n0 H13)))))) k H10 H11 (drop_gen_drop k x1 e x0 n0 
 H9)))))))))))) H4)) (csubst0_gen_head k c c2 t v i H2))))))))))) c1)))))) n).
+(* COMMENTS
+Initial nodes: 2989
+END *)
 
 theorem csubst0_drop_lt:
  \forall (n: nat).(\forall (i: nat).((lt n i) \to (\forall (c1: C).(\forall 
@@ -2292,6 +2298,9 @@ x6 x7 (refl_equal C (CHead x4 x3 x6)) (drop_drop (Flat f) n0 x1 (CHead x5 x3
 x7) H16 x0) H17 H18)) e H15)))))))))) H14)) H13)))))) k (drop_gen_drop k c e 
 t n0 H2) H8 H9) i H4))) c2 H5)))))))) H3)) (csubst0_gen_head k c c2 t v i 
 H1))))))))))) c1)))))) n).
+(* COMMENTS
+Initial nodes: 39886
+END *)
 
 theorem csubst0_drop_eq:
  \forall (n: nat).(\forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0 
@@ -4196,6 +4205,9 @@ C).(\lambda (_: T).(\lambda (_: T).(csubst0 O v e1 e2)))))) x3 x4 x5 x6 x7
 (Flat x3) x7) H15 x0) H16 H17)) e H14)))))))))) H13)) H12)))))))) k 
 (drop_gen_drop k c e t n0 H1) H3) c2 H4)))))))) H2)) (csubst0_gen_head k c c2 
 t v (S n0) H0))))))))))) c1)))) n).
+(* COMMENTS
+Initial nodes: 36162
+END *)
 
 theorem csubst0_drop_eq_back:
  \forall (n: nat).(\forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0 
@@ -6029,6 +6041,9 @@ C).(\lambda (_: C).(\lambda (u1: T).(\lambda (u2: T).(subst0 O v u1 u2))))))
 x3) x7)) (drop_drop (Flat f) n0 c (CHead x4 (Flat x3) x6) H16 t) H17 H18)) e 
 H15)))))))))) H14)) H13)))))))) k H3 (drop_gen_drop k x1 e x0 n0 H7)))))))))) 
 H2)) (csubst0_gen_head k c c2 t v (S n0) H0))))))))))) c1)))) n).
+(* COMMENTS
+Initial nodes: 34765
+END *)
 
 theorem csubst0_drop_lt_back:
  \forall (n: nat).(\forall (i: nat).((lt n i) \to (\forall (c1: C).(\forall 
@@ -6273,4 +6288,7 @@ C).(csubst0 (minus x2 (S n0)) v e1 e2)) (\lambda (e1: C).(drop (S n0) O
 H16 (drop_drop (Flat f) n0 c x H17 t)))))) H15)) H14))))))) k H9 H10 
 (drop_gen_drop k x1 e2 x0 n0 H8)) i H4))))))))))) H3)) (csubst0_gen_head k c 
 c2 t v i H1))))))))))) c1)))))) n).
+(* COMMENTS
+Initial nodes: 5939
+END *)