-fact drops_inv_cons_aux: ∀L1,L2,s,des. ⬇*[s, des] L1 ≡ L2 →
- ∀d,e,tl. des = {d, e} @ tl →
- ∃∃L. ⬇*[s, tl] L1 ≡ L & ⬇[s, d, e] L ≡ L2.
-#L1 #L2 #s #des * -L1 -L2 -des
-[ #L #d #e #tl #H destruct
-| #L1 #L #L2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
+fact drops_inv_cons_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 →
+ ∀l,m,tl. cs = {l, m} @ tl →
+ ∃∃L. ⬇*[s, tl] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
+#L1 #L2 #s #cs * -L1 -L2 -cs
+[ #L #l #m #tl #H destruct
+| #L1 #L #L2 #cs #l #m #HT1 #HT2 #l0 #m0 #tl #H destruct