Nuprl Definition : xxrefl

(!cond_cons(xxbasic; basic)):: refl(T;E) ==  Refl(T;x,y.E x y)


Definitions occuring in Statement :  refl: Refl(T;x,y.E[x; y]),  apply: f a
Definitions occuring in definition :  refl: Refl(T;x,y.E[x; y]),  apply: f a
Latex:
(!cond\_cons(xxbasic;  basic))::  refl(T;E)  ==    Refl(T;x,y.E  x  y)


Date html generated: 2016_05_15-PM-00_00_44
Last ObjectModification: 2015_09_23-AM-06_23_38

Theory : gen_algebra_1


Home Index