Nuprl - Some Definitions

nequal	`Def abT == a = b T` `Thm* x,y:A. xy Prop`
eq_int	`Def i=j == if i=jtrue; false fi` `Thm* i,j:. i=j`
bfalse	`Def false ==` `Thm* false`
bool	`Def == Unit+Unit` `Thm* Type`
btrue	`Def true ==` `Thm* true`
not	`Def A == A False` `Thm* (A) Prop`