Nuprl - Proof: equiv rel iff 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: equiv rel iff 1

Refl(Prop;A,B.A

B) & (Sym A,B:Prop. A

B) & (Trans A,B:Prop. A

By:	(Unfolds [`refl`;`sym`;`trans`] 0 THEN GenUnivCD) THEN HypBackchain

Generated subgoals:

None

About:

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