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.a  dom(f);1of(g)))
8. f  a:A fp-> B(a)
9. g  a:A fp-> B(a)
10. a  dom(f)
  a  dom(g)

1

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))

5 steps

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