-lemma llor_skip: ∀L1,L2,U,d. |L1| = |L2| → yinj (|L1|) ≤ d → L1 ⋓[U, d] L2 ≡ L1.
-#L1 #L2 #U #d #HL12 #Hd @and3_intro // -HL12
+lemma llor_skip: ∀L1,L2,U,l. |L1| = |L2| → yinj (|L1|) ≤ l → L1 ⋓[U, l] L2 ≡ L1.
+#L1 #L2 #U #l #HL12 #Hl @and3_intro // -HL12