This module contains the definition and rules for manipulating Leibniz (impredicative) equality. This file is based on the definitions in Randy Pollack's logic file.
** Module lib_eq_leibniz Imports lib_logic Eq = ... : {T|Type}T->T->Prop Eq_refl = ... : {T|Type}refl (Eq|T) Eq_subst = ... : {T|Type}{x,y|T}(Eq x y)->{P:T->Prop}(P x)->P y