Nuprl - Proof: fpf-cap-single

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

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

x : v(y)?z ~ if eqof(eq)(x,y)

v else z fi

By:	UnivCD THEN Repeat (Unfolds [`fpf-cap`;`fpf-single`;`fpf-ap`] 0) THEN Unfold `fpf-dom` 0 THEN Reduce 0 THEN SplitOnConclITE THEN SplitOnConclITE THEN Try Trivial THEN AllHyps ElimOrFalse

Generated subgoals:

None

About:

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