Nuprl Definition : refl

(basic):: Refl(T;x,y.E[x; y]) ==  ∀a:T. E[a; a]


Definitions occuring in Statement :  all: ∀x:A. B[x]
Definitions occuring in definition :  all: ∀x:A. B[x]
FDL editor aliases :  refl
Latex:
(basic)::  Refl(T;x,y.E[x;  y])  ==    \mforall{}a:T.  E[a;  a]


Date html generated: 2016_05_13-PM-04_14_36
Last ObjectModification: 2015_09_22-PM-05_46_02

Theory : rel_1


Home Index