lemma ldrop_ltpr_trans: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ➡ K2 →
∃∃L2. ⇩[d, e] L2 ≡ K2 & L1 ➡ L2.
#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
lemma ldrop_ltpr_trans: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ➡ K2 →
∃∃L2. ⇩[d, e] L2 ≡ K2 & L1 ➡ L2.
#L1 #K1 #d #e #H elim H -L1 -K1 -d -e