PrintForm
Definitions
mb
event
system
5
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-single-init
wf
x
:Id,
t
:Type,
v
:
t
.
x
:
t
initially
x
=
v
MsgA
By:
Auto THEN Unfold `ma-single-init` 0 THEN Analyze THEN Reduce 0
THEN
AssertBY (
x
:
t
x
:Id fp-> Type) Auto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
event
system
5
Sections
EventSystems
Doc
x:Id, t:Type, v:t. x : t initially x = v 
MsgA x:Id, t:Type, v:t. x : t initially x = v MsgA x:Id fp-> Type) Auto
