Nuprl - Proof: discrete vs bool 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: discrete vs bool 1 1

1. A : Type
2. (

x,y:A. Dec(x = y))

(

f:(A

x,y:A. (x f y)

x = y)

(A Discrete)

(

e:(A

x,y:A. (x e y)

x = y)

By:	Def of <type> Discrete

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html