English
Prepending an element and then flatMapping distributes as appending the mapped element and the rest: (l.cons a).flatMap f hf = (f a) appended to l.flatMap f hf.
Русский
Добавление элемента слева затем применение flatMap распределяется как добавление отображенного элемента к остальному: (l.cons a).flatMap f hf = (l.flatMap f hf).append (f a).
LaTeX
$$$\forall {\Gamma \Gamma'} [Inhabited(\Gamma)] [Inhabited(\Gamma')] (a : \Gamma) (l : ListBlank(\Gamma)) (f : \Gamma → List(\Gamma')) (hf) : (l.cons a).flatMap f hf = ListBlank.append (f a) (l.flatMap f hf)$$$
Lean4
@[simp]
theorem cons_flatMap {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (a : Γ) (l : ListBlank Γ) (f : Γ → List Γ') (hf) :
(l.cons a).flatMap f hf = (l.flatMap f hf).append (f a) :=
by
refine l.induction_on fun l ↦ ?_
simp only [ListBlank.append_mk, ListBlank.flatMap_mk, ListBlank.cons_mk, List.flatMap_cons]
