Its usage is
| where | eq_name | is the name of the equality predicate |
| eq_refl | is the name of its reflexivity proof | |
| eq_subst | is the name of its substitutivity proof |
The command first checks if the identifier eq_name_sym has been defined. If not, a proof of symmetry for eq_name is computed and called eq_name_sym. This done, it registers the name and the three theorems.
Note that if the symmetry proof is to be computed, the reflexivity and substitutivity proofs must already exist.
Note further that the appropriate Configure Equality command must be executed before any inductive declarations relying on it.
Configure Equality subsumes the previous Configure Qrepl command. (Indeed the former calls the latter.) Since Qrepl does not require equality to be reflexive (merely symmetric and substitutive), the old command is still available, enabling the use of Qrepl with partial equivalence relations.