Nuprl - Proof: fpf-join wf 1 2 1 1 1 2 1

(11steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc

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

1. A : Type
2. B : A

Type
3. f : d:A List

a:{a:A| (a

d) }

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

a:{a:A| (a

d) }

B(a)
5. eq : EqDecider(A)
6. a : A
7. (a

1of(g))
8. (

a.

deq-member(eq;a;1of(f)))(a)
9. g = g
10.

(a

1of(f))

deq-member(eq;a;1of(g))

By:	RWO Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) (x L) 0

Generated subgoals:

None

About:

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

(11steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc