Nuprl - Proof: subtype-fpf-cap

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: subtype-fpf-cap

X:Type, eq:EqDecider(X), f,g:x:X fp-> Type.

(

x:X. f(x)?Top

r g(x)?Top)

By:	Unfold `guard` 0 THEN Analyze 0 THEN All (Unfold `fpf-cap`) THEN MoveToConcl -1 THEN SplitOnConclITE THEN SplitOnConclITE THEN Unfold `fpf-sub` -5 THEN InstHyp [x] -5 THEN ExRepD

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html