If I am not mistaken, *Coq.Init.Wf* defines two transparent terms of precisely the same type, `well_founded_induction_type`

and `Fix`

. I understand how these functions “work” but I am not sure what the distinction is. Is there a strong reason to prefer `well_founded_induction_type`

when writing proofs?

It seems that `Fix`

is oriented towards defining recursive functions due to the rewriting lemma `Fix_eq`

. I also see that there are several functions named `well_founded_induction_<foo>`

with several values of `foo`

, so these are clearly intended as induction principles. But in what sense then is `well_founded_induction_type`

more oriented towards proofs than `Fix`

? In the recursion chapter of CPDT, Chlipala defines a function by `Fix`

and concludes the chapter with a comment I find cryptic:

One more piece of the full picture is missing. To go on and prove correctness of mergeSort, we would need more than a way of unfolding its definition. We also need an appropriate induction principle matched to the well-founded relation. Such a principle is available in the standard library, though we will say no more about its details here.

`Check well_founded_induction`

.

But I think any proof using `well_founded_induction_<foo>`

could just as easily be written with `Fix`

.

So why bother defining the induction principles?