why can acc eliminate into data?

Stream: new members

[Kenny Lau]

inductive acc {α : Sort u} (r : α → α → Prop) : α → Prop
| intro (x : α) (h : ∀ y, r y x → acc y) : acc x

/-
acc.rec_on :
  Π {α : Sort u_2} {r : α → α → Prop} {C : α → Sort u_1} {a : α},
    acc r a → (Π (x : α), (∀ (y : α), r y x → acc r y) → (Π (y : α), r y x → C y) → C x) → C a
-/

[Kenny Lau]

if acc is Prop, why can it eliminate into data?

[Floris van Doorn]

https://leanprover.github.io/reference/declarations.html#inductive-families

Generally speaking, for an inductive family in Prop, the motive in the eliminator is required to be in Prop. But there is an exception to this rule: you are allowed to eliminate from an inductively defined Prop to an arbitrary Sort when there is only one constructor, and each argument to that constructor is either in Prop or an index. The intuition is that in this case the elimination does not make use of any information that is not already given by the mere fact that the type of argument is inhabited. This special case is known as singleton elimination.