The next library equality file gives the definition and rules for Christine Paulin-Mohring's inductive equality. Loading this file causes the LEGO tactic Qrepl to be configured for this inductive equality.
** Mark "lib_ind_eq" **
Eq : {t|SET}t->t->Prop
Eqr : {t|SET}{x:t}Eq x x
Eq_elim : {t|SET}{x:t}{C_Eq:{x1|t}(Eq x x1)->TYPE}
(C_Eq (Eqr x))->{x1|t}{z:Eq x x1}C_Eq z
Eq_refl = ... : {t|SET}refl (Eq|t)
Eq_subst = ... : {t|SET}{m,n|t}(Eq m n)->{P:t->TYPE_minus1}(P m)->P n
Eq_sym = ... : {t|SET}sym (Eq|t)
Eq_trans = ... : {t|SET}trans (Eq|t)
Eq_resp = ... : {A,B|SET}{f:A->B}respect f Eq
Eq_resp2 = ... : {A,B,C|SET}{r:A->B->C}respect2 r Eq