Nuprl - Proof: fpf-join-ap 1

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

1. A : Type
2. B : A

Type
3. eq : EqDecider(A)
4. f : a:A fp-> B(a)
5. g : a:A fp-> B(a)
6. x : A
7. x

dom(f

g)
8.

dom(f)

dom(g)

By:	(RWO (Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. (Thm* x dom(f g) x dom(f) x dom(g) (-2) THEN (Analyze -2)

Generated subgoals:

None

About:

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