X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fetc%2Fldrop.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fetc%2Fldrop.etc;h=e4caef0c8d307f2cc9522f783fba268947f10b68;hb=5d669f492522b055f76c627eb89da97d0be05c2a;hp=0000000000000000000000000000000000000000;hpb=63c047cae0056da7a69cb0740336d12259fbeb1a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/etc/ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/etc/ldrop.etc
new file mode 100644
index 000000000..e4caef0c8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/etc/ldrop.etc
@@ -0,0 +1,11 @@
+lemma ldrop_bor1: ∀L1,L2,s1,s2,d,e. ⇩[s1, d, e] L1 ≡ L2 → ⇩[s1 ∨ s2, d, e] L1 ≡ L2.
+#L1 #L2 * /2 width=1 by ldrop_gen/
+qed.
+
+lemma ldrop_bor2: ∀L1,L2,s1,s2,d,e. ⇩[s2, d, e] L1 ≡ L2 → ⇩[s1 ∨ s2, d, e] L1 ≡ L2.
+#L1 #L2 #s1 #s2 >commutative_orb /2 width=1 by ldrop_bor1/
+qed.
+
+(* Basic_1: was: drop_conf_rev *)
+axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L →
+                 ∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1.