English
If a is in s, then there exists an index n such that some a ∈ get? s n.
Русский
Если a ∈ s, то найдётся индекс n, для которого some a ∈ get? s n.
LaTeX
$$$$\forall s:\\mathrm{WSeq}\,\alpha,\forall a:\\alpha,\ a \in s \Rightarrow \exists n,\text{some } a \in \mathrm{get?}\,s\,n.$$$$
Lean4
theorem get?_mem {s : WSeq α} {a n} : some a ∈ get? s n → a ∈ s :=
by
induction n generalizing s <;> intro h
case zero =>
rcases Computation.exists_of_mem_map h with ⟨o, h1, h2⟩
rcases o with - | o
· injection h2
injection h2 with h'
obtain ⟨a', s'⟩ := o
exact (eq_or_mem_iff_mem h1).2 (Or.inl h'.symm)
case succ n IH =>
have := @IH (tail s)
rw [get?_tail] at this
exact mem_of_mem_tail (this h)
