** Next:** Paulin-Mohring's Inductive Equality
** Up:** Equality
** Previous:** Martin-Löf's Inductive 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

*Lego*

*1998-06-15*