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