Library Equations.Classes
Require
Import
Relation_Definitions
.
A class for well foundedness proofs. Instances can be derived automatically using
Derive
Subterm
for
ind
.
Class
WellFounded
{
A
:
Type
} (
R
:
relation
A
) :=
wellfounded
:
well_founded
R
.