Paulin-Mohring's Inductive Equality

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
[[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