Nuprl - Proof: fpf-dom functionality2

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

A:Type, eq1,eq2:EqDecider(A), f:a:A fp-> Top, x:A. x

dom(f)

By:	Unfold `guard` 0 THEN Inst Thm* B:(AType), eq1,eq2:EqDecider(A), f:a:A fp-> B(a), x:A. Thm* x dom(f) = x dom(f) [A;a. Top;eq1;eq2;f;x] THEN HypSubst -1 0

Generated subgoals:

None

About:

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