Nuprl - Proof: fpf-join-dom 2

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

1. A : Type
2. B : A

Type
3. EqDecider(A)
4. f : d:A List

a:{a:A| (a

d) }

B(a)
5. g : d:A List

a:{a:A| (a

d) }

B(a)
6. x : A
7.

1of(f))

1of(g)) & True

1of(f))

1of(g))

By:	Auto THEN ParallelOp -1

Generated subgoals:

None

About:

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