1. A : Type
2. B : AType
3. f : d:A Lista:{a:A| (a  d) }B(a)
4. g : d:A Lista:{a:A| (a  d) }B(a)
5. eq : EqDecider(A)
6. a : A
7. (a  1of(f) @ filter(a.deq-member(eq;a;1of(f));1of(g)))
8. f  a:A fp-> B(a)
9. g  a:A fp-> B(a)
10. deq-member(eq;a;1of(f))
  deq-member(eq;a;1of(g))

By:	RWO Thm* x:T, l1,l2:T List. (x  l1 @ l2)  (x  l1)  (x  l2) -4 THEN Analyze -2

1

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

4 steps

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