# What is the canonical eliminator for Acc? Why uses Fix_F a nested match?

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`.

Interesting question. I suppose the extractions are the same? In that case, the only difference is that elim2 delays the pattern-matching on the proof so you might get better equalities on open terms with it (e.g I you reduce on an axiomatized accessibility proof). The downside however is that in cbv you will reduce it multiple times… I guess some benchmarking is necessary. Regarding Function/Equations I think they will be insensitive to that, unless you can’t prove the same unfolding lemmas on elim1 and elim2.