A:Type, eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top.
  f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi

By:

UnivCD THEN Unfold `fpf-cap` 0 THEN RWO Thm* eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A. Thm* f  g(x) ~ if x  dom(f) f(x) else g(x) fi 0 THEN Repeat SplitOnConclITE THEN Try Trivial THEN All (RWO (Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. (Thm* x  dom(f  g)  x  dom(f)  x  dom(g)) THEN SplitOrHyps THEN Try Trivial THEN AllHyps (h.Analyze h THEN OrLeft THEN Complete Auto) THEN AllHyps (h.Analyze h THEN OrRight THEN Complete Auto)

None

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