Library `Coq.Init.Wf`

defines a well-founded fixed point operator `Fix_F`

. The definition is nonstandard (I think) since it uses a nested match rather than a top-level match. Below appear two eliminators for Acc where `elim1`

is a standard eliminator with a top level match and `elim2`

is an eliminator using a nested match similar to `Fix_F`

.

```
Section Acc.
Variable X : Type.
Variable R : X -> X -> Prop.
Variable P : X -> Type.
Variable F : forall x, (forall y, R y x -> P y) -> P x.
Fixpoint elim1 (x : X) (a : Acc R x) : P x :=
let (h) := a in F x (fun y r => elim1 y (h y r)).
Fixpoint elim2 (x : X) (a : Acc R x) : P x :=
F x (fun y r => elim2 y (let (h) := a in h y r)).
End Acc.
```

I’m curious whether using `elim2`

is essential for applications, in particular the Equations plugin, or whether `elim1`

would suffice. My guess is that `elim1`

suffices. In other words, was it a deliberate decision to have `elim2`

rather than `elim1`

?

The background of my question is the quest for a kernel without match and fix but rather a single eliminator for every inductive type. I think of `elim1`

as the canonical eliminator for `Acc`

.