Nuprl - Proof: fpf-single-dom-sq

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-single-dom-sq

A:Type, eq:EqDecider(A), x,y:A, v:Top. x

dom(y : v) ~ (eqof(eq)(y,x))

By:	UnivCD THEN Unfolds [`fpf-dom`;`fpf-single`] 0 THEN Reduce 0 THEN AutoBoolCase (eqof(eq)(y,x))

Generated subgoals:

None

About:

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