Nuprl - Proof: type def iso

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: type def iso

'a,'b:S, P:('b

), rep:('a

'b), abs:('b

'a).

iso_pair('a;'b;P;rep;abs)

(

rep':('a

'b). type_definition('b;'a;P;rep'))

By:	Id THEN StrongAuto THEN Unab [`iso_pair`] THEN DTerm rep 0 THEN StrongAuto

Generated subgoals:

None

About:

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