X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fdrop%2Fprops.ma;h=1d662e8d45b075b64650974e49b51cb9f3021f9d;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=6ea5bca4cfa60b40a9afdbe77afd40300f8268ee;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/drop/props.ma b/matita/matita/contribs/lambdadelta/basic_1/drop/props.ma
index 6ea5bca4c..1d662e8d4 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/drop/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/drop/props.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/drop/fwd.ma".
 
-theorem drop_skip_bind:
+lemma drop_skip_bind:
  \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h 
 d c e) \to (\forall (b: B).(\forall (u: T).(drop h (S d) (CHead c (Bind b) 
 (lift h d u)) (CHead e (Bind b) u))))))))
@@ -26,7 +26,7 @@ d c e) \to (\forall (b: B).(\forall (u: T).(drop h (S d) (CHead c (Bind b)
 d) (\lambda (n: nat).(drop h (S d) (CHead c (Bind b) (lift h n u)) (CHead e 
 (Bind b) u))) (drop_skip (Bind b) h d c e H u) d (refl_equal nat d)))))))).
 
-theorem drop_skip_flat:
+lemma drop_skip_flat:
  \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h 
 (S d) c e) \to (\forall (f: F).(\forall (u: T).(drop h (S d) (CHead c (Flat 
 f) (lift h (S d) u)) (CHead e (Flat f) u))))))))
@@ -37,7 +37,7 @@ f) d) (\lambda (n: nat).(drop h (S d) (CHead c (Flat f) (lift h n u)) (CHead
 e (Flat f) u))) (drop_skip (Flat f) h d c e H u) (S d) (refl_equal nat (S 
 d))))))))).
 
-theorem drop_ctail:
+lemma drop_ctail:
  \forall (c1: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop 
 h d c1 c2) \to (\forall (k: K).(\forall (u: T).(drop h d (CTail k u c1) 
 (CTail k u c2))))))))