(9steps total)
PrintForm
Definitions
mb
event
system
1
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fun
exp
add
sq
1
m
:
,
f
,
i
:Top. (
f
^0+
m
(
i
)) ~ (
f
^0(
f
^
m
(
i
)))
By:
Analyze 0 THEN Subst ((0+
m
) ~
m
) 0 THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(9steps total)
PrintForm
Definitions
mb
event
system
1
Sections
EventSystems
Doc
m:
, f,i:Top. (f^0+m(i)) ~ (f^0(f^m(i))) m:, f,i:Top. (f^0+m(i)) ~ (f^0(f^m(i)))
