English
If some (a', s') is in the destruct of s, then for any a, a ∈ s is equivalent to a = a' or a ∈ s'.
Русский
Если some (a', s') принадлежит разбивке по destruct(s), то для любого a выполняется a ∈ s ⇔ a = a' ∨ a ∈ s'.
LaTeX
$$$$\forall s:\\mathrm{WSeq}\,\alpha,\forall a,a':\alpha,\forall s':\\mathrm{WSeq}\,\alpha,\ \text{some}(a',s') \in \mathrm{destruct}\,s \to \left(a \in s \iff a = a' \lor a \in s'\right).$$$$
Lean4
theorem eq_or_mem_iff_mem {s : WSeq α} {a a' s'} : some (a', s') ∈ destruct s → (a ∈ s ↔ a = a' ∨ a ∈ s') :=
by
generalize e : destruct s = c; intro h
revert s
apply Computation.memRecOn h <;> [skip; intro c IH] <;> intro s <;> induction s using WSeq.recOn <;> intro m <;>
have := congr_arg Computation.destruct m <;>
simp at this
· obtain ⟨i1, i2⟩ := this
rw [i1, i2]
obtain ⟨f, al⟩ := s'
dsimp only [cons, Membership.mem, WSeq.Mem, Seq.Mem, Seq.cons]
have h_a_eq_a' : a = a' ↔ some (some a) = some (some a') := by simp
rw [h_a_eq_a']
refine ⟨Stream'.eq_or_mem_of_mem_cons, fun o => ?_⟩
· rcases o with e | m
· rw [e]
apply Stream'.mem_cons
· exact Stream'.mem_cons_of_mem _ m
· simp [IH this]
