The next library equality file gives the definition and rules for Christine Paulin-Mohring's inductive equality.
** Module lib_eq_inductive Imports lib_logic $Eq : {t|Type}t->t->Prop $Eqr : {t|Type}{x:t}Eq x x $Eq_elim : {t|Type}{x:t}{C_Eq:{x1|t}(Eq x x1)->Type}(C_Eq (Eqr x))->{x1|t} {z:Eq x x1}C_Eq z ** Label (!Eq!) Eq ** Label (!Eq elim!) Eq_elim ** Label (!Eq Eqr!) Eqr [[t|Type][x:t][C_Eq:{x1|t}(Eq x x1)->Type][f_Eqr:C_Eq (Eqr x)] Eq_elim x C_Eq f_Eqr (Eqr x) ==> f_Eqr] Eq_refl = ... : {t|Type}refl (Eq|t) Eq_subst = ... : {t|Type}{m,n|t}(Eq m n)->{P:t->Type}(P m)->P n