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.

** Mark "lib_ML_eq" ** Eq : {t|SET}t->t->Prop Eqr : {t|SET}{x:t}Eq x x Eq_elim : {t|SET}{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 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

Fri May 24 19:01:27 BST 1996