Nuprl - Proof: nat sq

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat sq

SQType(

)

By:	Unfold `sq_type` 0 THEN UnivCD

Generated subgoal:

1 1. x :
2. y :
3. x = y
x ~ y
1 step

About:

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