(2steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime
decider
exists
!
{
p
:(
)|
x
:
.
p
(
x
)
prime(
x
) }
By:
BackThru:
Thm*
P
:(
A
Type). (
x
:
A
. Dec(
P
(
x
)))
(
!
{
p
:(
A
)|
x
:
A
.
p
(
x
)
P
(
x
) })
Generated subgoal:
1
x
:
. Dec(prime(
x
))
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
!
{p:(
)| 
x:. p(x) 
prime(x) } !{p:()| x:. p(x) prime(x) }P:(AType). (x:A. Dec(P(x))) 
(!{p:(A)| x:A. p(x) P(x) }) x:. Dec(prime(x))
