By default, the library provides Martin-Löf equality. Users who
wish to work with a different notion of equality need to implement
their own version of the module `lib_eq` and ensure that the
`LEGOPATH` respects their choice . Provided this
exports a relation `Eq`, a proof of its reflexivity and
substitutivity `Eq_refl`, `Eq_subst`, the module
`lib_eq_basics` will generate some theorems and configures
the commands `Qrepl`, `Induction`, `Qnify` and
the switch `Theorems`.

For convenience, a definition of Leibniz equality can be copied from
the module `lib_eq_leibniz` and Christine Paulin-Mohring's
inductive equality from `lib_eq_inductive`.