English
If b ∈ bind s f, then ∃ a ∈ s, b ∈ f a (via map and join).
Русский
Если b ∈ bind s f, то существует a ∈ s, такое что b ∈ f(a) (через map и join).
LaTeX
$$$$ b \\in (s \\mathbin{\\text{bind}} f) \\Rightarrow \\exists a \\in s, b \\in f(a) $$$$
Lean4
/-- Replace the `n`th element of `s` with `a`. -/
def updateNth (s : WSeq α) (n : ℕ) (a : α) : WSeq α :=
@Seq.corec (Option α) (ℕ × WSeq α)
(fun ⟨n, s⟩ =>
match Seq.destruct s, n with
| none, _ => none
| some (none, s'), n => some (none, n, s')
| some (some a', s'), 0 => some (some a', 0, s')
| some (some _, s'), 1 => some (some a, 0, s')
| some (some a', s'), n + 2 => some (some a', n + 1, s'))
(n + 1, s)
