Nuprl - Proof: fpf-single-dom 1

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

1. A : Type
2. eq : EqDecider(A)
3. x : A
4. y : A
5. v : Top

dom(y : v)

x = y

By:	Unfolds [`fpf-dom`;`fpf-single`] 0 THEN Reduce 0 THEN RW assert_pushdownC 0

Generated subgoal:

1 eqof(eq)(y,x) False x = y
1 step

About:

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