Martin-Löf's Inductive Equality

  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.

 ** Module lib_eq Imports lib_logic
 $Eq : {t|Type}t->t->Prop
 $Eqr : {t|Type}{x:t}Eq x x
 $Eq_elim :
    {t|Type}{P:{x,y:t}(Eq x y)->Type}({x:t}P x x (Eqr x))->{x,y:t}
    {p:Eq x y}P x y p
[[t:Type][P:{x,y:t}(Eq x y)->Type][h:{x:t}P x x (Eqr x)][x:t]
    Eq_elim P h x x (Eqr x)  ==>  h x]

  Eq_refl = ... : {t|Type}refl (Eq|t)
  Eq_subst = ... : {t|Type}{m,n|t}(Eq m n)->{P:t->Type}(P m)->P n
  trivType = ... : Type
  emptyType = ... : Type
 ** Config Theorems trivType emptyType Eq_subst