(2steps total)
PrintForm
Definitions
Lemmas
mb
event
system
4
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-single
wf
A
:Type,
B
:(
A
Type),
x
:
A
,
v
:
B
(
x
).
x
:
v
x
:
A
fp->
B
(
x
)
By:
Unfolds [`fpf`;`fpf-single`] 0 THEN Analyze -1
THEN
RWO
Thm*
a
,
x
:
T
. (
x
[
a
])
x
=
a
-1
Generated subgoal:
1
1.
A
: Type
2.
B
:
A
Type
3.
x
:
A
4.
v
:
B
(
x
)
5.
x1
:
A
6.
x1
=
x
v
B
(
x1
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
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:Type, B:(AType), x:A, v:B(x). x : v x:A fp-> B(x)a,x:T. (x [a]) 
x = a -1Type
v B(x1)
