/2 width=3/ qed-.
lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 →
/2 width=3/ qed-.
lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 →
(* Basic properties *********************************************************)
lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 →
(* Basic properties *********************************************************)
lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 →