Nuprl - Proof: fpf-sub-join-left

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

A:Type, B1,B2:(A

Type), eq:EqDecider(A), f:a:A fp-> B1(a),

g:a:A fp-> B2(a). f

By:	Auto THEN Unfolds [`fpf-sub`] 0 THEN Try (RWO (Thm* B,C:(AType), eq:EqDecider(A), f:a:A fp-> B(a), g:a:A fp-> C(a), x:A. (Thm* x dom(f) f g(x) = f(x) B(x) (0) THEN Try (RWO (Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A. (Thm* x dom(f g) x dom(f) x dom(g) (0 (THEN (OrLeft)

Generated subgoals:

None

About:

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