(7steps total)
PrintForm
Definitions
mb
event
system
6
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable-exists-finite
1
1
1
1.
T
: Type
2.
P
:
T
Prop
3.
x
:
T
. Dec(
P
(
x
))
4.
n
:
5.
f
:
n
T
6.
b
:
T
.
a
:
n
.
f
(
a
) =
b
7.
x
:
T
8.
P
(
x
)
i
:
n
.
P
(
f
(
i
))
By:
InstHyp [
x
] -3 THEN ParallelOp -1
Generated subgoal:
1
9.
a
:
n
10.
f
(
a
) =
x
P
(
f
(
a
))
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
mb
event
system
6
Sections
EventSystems
Doc
Prop
x:T. Dec(P(x))
a:
