Nuprl - Proof: fpf-single-dom 1 1

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

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

eqof(eq)(y,x)

False

x = y

By:	RWO "deq_property<" 0 THEN SplitOrHyps THEN OrLeft

Generated subgoals:

None

About:

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