Type mismatch with projection notation

Stream: lean4

[Scott Morrison]

Can someone explain what is going on here:

/-- `IsEmpty α` expresses that `α` is empty. -/
class IsEmpty (α : Sort _) : Prop where
  protected false : α → False

/-- Eliminate out of a type that `IsEmpty` (without using projection notation). -/
@[elab_as_elim]
def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a :=
  (IsEmpty.false a).elim

example {α : Type u} [IsEmpty α] (x : α) : none = some x := isEmptyElim x -- works

/-- Eliminate out of a type that `IsEmpty` (using projection notation). -/
protected def IsEmpty.elim (_ : IsEmpty α) {p : α → Sort _} (a : α) : p a :=
  isEmptyElim a

example {α : Type u} (h : IsEmpty α) (x : α) : none = some x := h.elim x -- fails

[Parth Shastri]

This example seems to work if you add @[elab_as_elim] to IsEmpty.elim.