Theorem: List.pure_bind (Extra/List.lean)

State before:
α : Type u_1
β : Type u_2
f : α → List β
a : α
⊢ [a].bind f = f a
Tactic:
rw [cons_bind, nil_bind, append_nil]
State after:
no goals