lemma drops_drop_trans: ∀L1,L,cs. ⬇*[Ⓕ, cs] L1 ≡ L → ∀L2,i. ⬇[i] L ≡ L2 →
∃∃L0,cs0,i0. ⬇[i0] L1 ≡ L0 & ⬇*[Ⓕ, cs0] L0 ≡ L2 &
- @â¦\83i, csâ¦\84 â\89¡ i0 & cs â\96 i â\89¡ cs0.
+ @â\9dªi, csâ\9d« â\89\98 i0 & cs â\96 i â\89\98 cs0.
#L1 #L #cs #H elim H -L1 -L -cs
[ /2 width=7 by drops_nil, minuss_nil, at_nil, ex4_3_intro/
| #L1 #L0 #L #cs #l #m #_ #HL0 #IHL0 #L2 #i #HL2