Nuprl - Proof: card quotient 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card quotient 1 1

1. A : Type
2. E : A

Prop
3. EquivRel a,a':A. E(a;a')

InvFuns(q:A/E

{x:A| q = x };A;

qx.qx/q,x. x;

x.<x,x>)

By:	Analyze THEN Reduce Concl THEN Rename-1: qx

Generated subgoal:

1 4. qx : q:A/E{x:A| q = x }
<qx/q,x. x,qx/q,x. x> = qx q:A/E{x:A| q = x }
3 steps

About:

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