{ rintro (h | h)
  { simp[h] }
  { have := ih.mpr h; simp[this] } }
case cons.mpr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (f a = none ∨ ∃ a ∈ l, f a = none) → ∀ (a_2 : β), f a = some a_2 → ∀ (a : List β), ¬mapM' f l = some a
no goals