-| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K1 #e #H
- elim (ldrop_inv_O1 … H) -H * #He #HLK1
+| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #_ #IHL12 #K1 #e #H
+ elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1
(* Note: the constant 0 cannot be generalized *)
lemma lsubss_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
(* Note: the constant 0 cannot be generalized *)
lemma lsubss_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
-| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K2 #e #H
- elim (ldrop_inv_O1 … H) -H * #He #HLK2
+| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #_ #IHL12 #K2 #e #H
+ elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2