English
If some a ∈ s.tail.destruct, then there exists a' with some a' ∈ s.destruct.
Русский
Если some a входит в s.tail.destruct, то существует a' такое, что some a' входит в s.destruct.
LaTeX
$$$$\text{some } a \in \operatorname{destruct}(\operatorname{tail}(s)) \Rightarrow \exists a'\,\text{some } a' \in \operatorname{destruct}(s).$$$$
Lean4
theorem destruct_some_of_destruct_tail_some {s : WSeq α} {a} (h : some a ∈ destruct (tail s)) :
∃ a', some a' ∈ destruct s := by
unfold tail Functor.map at h; simp only [destruct_flatten] at h
rcases exists_of_mem_bind h with ⟨t, tm, td⟩; clear h
rcases Computation.exists_of_mem_map tm with ⟨t', ht', ht2⟩; clear tm
rcases t' with - | t' <;> rw [← ht2] at td <;> simp only [destruct_nil] at td
· have := mem_unique td (ret_mem _)
contradiction
· exact ⟨_, ht'⟩
