dependent induction is not documented in the manual

[SimonBoulier]

Also there is something very confusing. As far as I understand:

Require Import Program.
From Equations Require Import Equations.

will use dependent induction of Program.

But

Require Import Program.
From Equations Require Import Equations.
Require Import Equations.Prop.DepElim.

will use dependent induction of Equations. :-)

[mattam82]

Yes, that needs to be sorted out, maybe dependent induction should just be exported by Equations always.