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