mapM lemmas missing for `M:=list`
mapM : (A → M B) → list A → M (list B)
is parametric in a monad M
. We have lemmas for M
being a set and being option, but those for M
being list are missing.
Also the lemmas and naming for sets and option are pretty inconsistent. Would be good to improve that once we add lists.