This library file gives the definition and rules for Martin-Löf's
inductive equality.  We cannot use LEGO's inductive type mechanism for
this definition because the type of the constructor Eqr does not
conform to Luo's schema for inductive types, so the definition is done
by hand.  Loading this file causes the LEGO tactic Qrepl to be
configured for this inductive equality.