+lemma ldrop_fwd_length_eq: ∀L1,L2,K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ |L1| = |L2| → |K1| = |K2|.
+#L1 #L2 #K1 #K2 #d #e #HLK1 #HLK2 #HL12
+lapply (ldrop_fwd_length … HLK1) -HLK1
+lapply (ldrop_fwd_length … HLK2) -HLK2
+/2 width=2 by injective_plus_r/ (**) (* full auto fails *)
+qed-.
+