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

Using Rocq
1

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.

2

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.