Nuprl - Proof: fpf-join-ap-left

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-join-ap-left

A:Type, B,C:(A

Type), eq:EqDecider(A), f:a:A fp-> B(a), g:a:A fp-> C(a),

x:A. x

dom(f)

g(x) = f(x)

B(x)

By:	Auto THEN Unfolds [`fpf-join`;`fpf-ap`] 0 THEN Reduce 0 THEN Subst ((2of(f)(x)) ~ f(x)) 0 THEN Try (Unfold `fpf-ap` 0 THEN Trivial) THEN Unfold `fpf-cap` 0 THEN SplitOnConclITE

Generated subgoals:

None

About:

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