Leibniz Equality

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