cases hb : f a <;> simp
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ¬∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    none
case some
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ¬∃ b, f a = some b
val✝ : β
hb : f a = some val✝
⊢ False