A typeclass to ease the handling of decidable properties.
A proposition is decidable whenever it is reflected by a boolean.
Alternative ways of specifying the reflection property.
The generic function that should be used to program, together with some
useful tactics.
Some usual instances.