The example in the manual doesn't show the difference between the Induction and Elimination principles generated by Scheme.
I also imagined the Elimination principle would have type
forall P : Nat -> Set, P z -> (forall n : Nat, P (s n)) -> forall n : Nat, P n instead of the same one as the Induction Principle.
Why are they in fact the same ?
It seems Elimination and Case are the same as Induction and Minimality respectively except for naming, and have been that way since they were introduced in https://github.com/coq/coq/commit/ba360bdefa2d7e4200c94a37c5065019718c2691
Last updated: Oct 04 2023 at 22:01 UTC