Nuprl - Proof: is one one corr rel wf

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: is one one corr rel wf

A,B:Type, R:(A

Prop). (1-1-Corr x:A,y:B. R(x;y))

Prop

By:	Def of 1-1-Corr [var]:<type>,[var]:<type>. <prop>

Generated subgoals:

None

About:

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