next up previous contents
Next: Paulin-Mohring's Inductive Equality Up: Equality Previous: Equality

Leibniz Equality

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



Lego
Fri May 24 19:01:27 BST 1996