]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2A/etc/etc/ldrop.etc
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / etc / etc / ldrop.etc
1 lemma ldrop_bor1: ∀L1,L2,s1,s2,d,e. ⇩[s1, d, e] L1 ≡ L2 → ⇩[s1 ∨ s2, d, e] L1 ≡ L2.
2 #L1 #L2 * /2 width=1 by ldrop_gen/
3 qed.
4
5 lemma ldrop_bor2: ∀L1,L2,s1,s2,d,e. ⇩[s2, d, e] L1 ≡ L2 → ⇩[s1 ∨ s2, d, e] L1 ≡ L2.
6 #L1 #L2 #s1 #s2 >commutative_orb /2 width=1 by ldrop_bor1/
7 qed.
8
9 (* Basic_1: was: drop_conf_rev *)
10 axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L →
11                  ∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1.