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.