The first contains the definition and rules for manipulating Leibniz (impredicative) equality. Loading this file causes the LEGO tactic Qrepl to be configured for Leibniz equality. This file is based on the definitions in Randy Pollack's logic file.
** 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