A:Type, B:(AType), eq1,eq2:EqDecider(A), f:a:A fp-> B(a), x:A.
  x  dom(f) = x  dom(f)  

By:	Auto THEN Unfold `fpf-dom` 0 THEN Analyze -2 THEN Reduce 0 THEN AutoBoolCase deq-member(eq1;x;d) THEN AutoBoolCase deq-member(eq2;x;d) THEN All (RWO Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L))

None

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