(2steps total)
PrintForm
Definitions
mb
event
system
3
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-empty
wf
A
:Type,
B
:(
A
Type).
x
:
A
fp->
B
(
x
)
By:
Unfolds [`fpf`;`fpf-empty`] 0
Generated subgoal:
1
1.
A
: Type
2.
B
:
A
Type
3.
x
: {
x
:
A
| (
x
nil) }
4.
=
5.
zzz
: Unit
zzz
B
(
x
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
mb
event
system
3
Sections
EventSystems
Doc
A:Type, B:(A
Type). 
x:A fp-> B(x) A:Type, B:(AType). x:A fp-> B(x)Type
nil) }
=
zzz B(x)
