English
If types match (β = β') and for all a ∈ m we have f a ≍ f' a (heterogeneous equivalence), then bind m f ≍ bind m f'.
Русский
Если типы совпадают (β = β') и для всех a ∈ m выполняется f a ≍ f' a (гетерогенная эквивалентность), тогда bind m f ≍ bind m f'.
LaTeX
$$$\\forall {β' : Type v}, {m : Multiset α}, {f : α → Multiset β}, {f' : α → Multiset β'}, (h : β = β') \\rightarrow (\\forall a ∈ m, f a \\stackrel{HEq}{\\cong} f' a) \\rightarrow m.bind f \\stackrel{HEq}{\\cong} m.bind f'$$$
Lean4
theorem bind_hcongr {β' : Type v} {m : Multiset α} {f : α → Multiset β} {f' : α → Multiset β'} (h : β = β')
(hf : ∀ a ∈ m, f a ≍ f' a) : bind m f ≍ bind m f' :=
by
subst h
simp only [heq_eq_eq] at hf
simp [bind_congr hf]
