mb
event
system
4
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
A
:Type,
B
:(
A
Type),
x
:
A
,
v
:
B
(
x
).
x
:
v
x
:
A
fp->
B
(
x
)
[fpf-single_wf]
cites the following:
Thm*
a
,
x
:
T
. (
x
[
a
])
x
=
a
[member_singleton]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
event
system
4
Sections
EventSystems
Doc
A:Type, B:(A
Type), x:A, v:B(x). x : v 
x:A fp-> B(x)a,x:T. (x [a]) 
x = aA:Type, B:(AType), x:A, v:B(x). x : v x:A fp-> B(x)a,x:T. (x [a]) x = a