-lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ÷⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. K1 ÷⊑ K2 & ⇩[0, e] L1 ≡ K1.
+(* Note: the constant 0 cannot be generalized *)
+lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1.