milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / etc / etc / ldrop.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/etc/etc/ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2A/etc/etc/ldrop.etc
new file mode 100644 (file)
index 0000000..e4caef0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2A/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.