English
If a ∈ s, then there exist n and s' with some (a, s') in the destruct of the dropped sequence.
Русский
Если a ∈ s, то существуют n и s', для которых some (a, s') встречается в destruct( drop s n ).
LaTeX
$$$$\forall s:\\mathrm{WSeq}\,\alpha,\forall a:\\alpha,\ a \in s \Rightarrow \exists n\exists s',\text{some }(a,s') \in \mathrm{destruct}(\mathrm{drop}\,s\,n).$$$$
Lean4
theorem exists_dropn_of_mem {s : WSeq α} {a} (h : a ∈ s) : ∃ n s', some (a, s') ∈ destruct (drop s n) :=
let ⟨n, h⟩ := exists_get?_of_mem h
⟨n, by
rcases (head_terminates_iff _).1 ⟨⟨_, h⟩⟩ with ⟨⟨o, om⟩⟩
have := Computation.mem_unique (Computation.mem_map _ om) h
rcases o with - | o
· injection this
injection this with i
obtain ⟨a', s'⟩ := o
dsimp at i
rw [i] at om
exact ⟨_, om⟩⟩
