Nuprl - Proof: fpf-join-dom 1

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

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. (x

1of(f))

1of(g)) & False

1of(f))

1of(g))

By:	Auto THEN OrLeft

Generated subgoals:

None

About:

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