IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-single-effect1 wf1111 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)
11. x dom(x : A)
y : B(x)?Void = A Type
By:
Analyze -1
THEN
RWO Thm*eq:EqDecider(A), x,y:A, v:Top. x dom(y : v) x = y 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html