A:Type, B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
  x  dom(f  g)  x  dom(f)  x  dom(g)

By:

Unfolds [`fpf`;`fpf-join`;`fpf-dom`] 0 THEN Unfold `fpf-dom` 0 THEN Reduce 0 THEN UnivCD THEN RWO Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L) 0 THEN RWO Thm* x:T, l1,l2:T List. (x  l1 @ l2)  (x  l1)  (x  l2) 0 THEN RWO Thm* P:(T), L:T List, x:T. (x  filter(P;L))  (x  L) & P(x) 0 THENA Reduce 0 THEN Reduce 0 THEN AutoBoolCase deq-member(eq;x;1of(f)) THEN RWO Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L) -1

1	1. A : Type 2. B : AType 3. EqDecider(A) 4. f : d:A Lista:{a:A| (a  d) }B(a) 5. g : d:A Lista:{a:A| (a  d) }B(a) 6. x : A 7. (x  1of(f))   (x  1of(f))  (x  1of(g)) & False  (x  1of(f))  (x  1of(g))	1 step
2	1. A : Type 2. B : AType 3. EqDecider(A) 4. f : d:A Lista:{a:A| (a  d) }B(a) 5. g : d:A Lista:{a:A| (a  d) }B(a) 6. x : A 7. (x  1of(f))   (x  1of(f))  (x  1of(g)) & True  (x  1of(f))  (x  1of(g))	1 step

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