lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
∃∃K1. K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1.
#L1 #L2 #H elim H -L1 -L2
lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
∃∃K1. K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1.
#L1 #L2 #H elim H -L1 -L2