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

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

filter(

a.

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

(a

1of(f))

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

By:	RWO Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x) -3

Generated subgoal:

1 7. (a  1of(g))
8. (a.deq-member(eq;a;1of(f)))(a)
9. g = g  a:A fp-> B(a)
10. (a  1of(f))
  deq-member(eq;a;1of(g))
1 step

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