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