Map M for M

public theorem mapM_forM {α β : Type} (f : α → Except β PUnit) (xs : List α) (ys : List PUnit) :  xs.mapM f = Except.ok ys → xs.forM f = Except.ok ():= by  intro h₀  induction xs generalizing ys with  | nil => simp only [forM_eq_forM, forM_nil]; rfl  | cons xh xt ih =>    simp only [forM_eq_forM, forM_cons]    cases h₁ : f xh with    | error =>      simp only [List.mapM_cons] at h₀      rw [h₁] at h₀      simp only [Except.bind_err, reduceCtorEq] at h₀    | ok =>        simp only [List.mapM_cons, pure, Except.pure] at h₀        cases h₁ : f xh <;>        simp only [h₁, Except.bind_err, Except.bind_ok, reduceCtorEq] at h₀        rename_i yh        cases h₂ : List.mapM f xt <;>        simp only [h₂, Except.bind_err, Except.bind_ok, reduceCtorEq] at h₀        rename_i yt        simp only [Except.ok.injEq] at h₀        subst h₀        simp only [Except.bind_ok]        apply ih yt        assumption