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.