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

By:

Auto THEN Unfolds [`fpf-sub`] 0 THEN Try (RWO (Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. (Thm* x  dom(f  g)  f  g(x) = if x  dom(f) f(x) else g(x) fi  B(x) (0) THEN Try ((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) ((0) (THEN (OrRight) THEN SplitOnConclITE THEN Reduce 0

1

1. A : Type 2. B : AType 3. eq : EqDecider(A) 4. f : a:A fp-> B(a) 5. g : a:A fp-> B(a) 6. f || g 7. x : A 8. x  dom(g) 9. x  dom(f)   g(x) = f(x)  B(x)

1 step

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