IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
effect-rule11222211 1. Id
2. x : Id
3. y : Id
4. k : Knd
5. T : Type
6. A : Type
7. B : Type
8. ABTA 9. y = x 10. x : Ay : Bx:Id fp-> Type
11. k : Tk:Knd fp-> Type
12. s : x@0:Idx : Ay : B(x@0)?Top
13. v : ma-valtype(k : T; k)
14. x : Ay : B(x)?Void = A 15. x : Ay : B(x)?Top = A 16. z : A 17. s(x) = z 18. vT x : Ay : B(y)?Top r B
By:
RWO
Thm*eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top.
Thm* fg(x)?z ~ if x dom(f)f(x)?z else g(x)?z fi
0
THEN
SplitOnConclITE
THEN
Reduce 0