English
If s1 ~ʷ s2 and for all a, f1 a ~ʷ f2 a, then (s1.bind f1) ~ʷ (s2.bind f2).
Русский
Если s1 эквивалентно s2 и для каждого элемента a выполняется f1 a ~ʷ f2 a, то (s1.bind f1) эквивалентно (s2.bind f2).
LaTeX
$$$ \forall {s1 s2 : \mathrm{WSeq}\,\alpha}, {f1 f2 : \alpha \to \mathrm{WSeq}\,\beta},\; s1 \sim_W s2 \to (\forall a, f1 a \sim_W f2 a) \Rightarrow (s1.bind f1) \sim_W (s2.bind f2)$$$
Lean4
@[simp]
theorem bind_assoc_comp (s : WSeq α) (f : α → WSeq β) (g : β → WSeq γ) :
bind (bind s f) g ~ʷ bind s ((fun y : WSeq β => bind y g) ∘ f) :=
by
simp only [bind, map_join]
rw [← map_comp f (map g), ← Function.comp_def, comp_assoc, map_comp (map g ∘ f) join s]
exact join_join (map (map g ∘ f) s)
