IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-single-effect1 wf111 1. x : Id
2. y : Id
3. k : Knd
4. A : Type
5. B : Type
6. T : Type
7. ABTA 8. y = x 9. State(x : Ay : B)
10. ma-valtype(k : T; k)
x : Ay : B(x)?Void = A Type
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