(7steps total)
PrintForm
Definitions
Lemmas
hol
bool
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hexists
def
'a
:S. equal(exists,
P
:
'a
hbool.
P
(select(
P
)))
By:
Simpset [`hol_to_nuprl`]
Generated subgoal:
1
'a
:S. (
p
:
'a
.
x
:
'a
. (
p
(
x
))) =
(
P
:
'a
.
P
(@
x
:
'a
. (
P
(
x
))))
6
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
hol
bool
Sections
HOLlib
Doc
'a:S. equal(exists,
P:'a 
hbool. P(select(P))) 'a:S. equal(exists,P:'a hbool. P(select(P))) 'a:S. (p:'a
. 
x:'a. (p(x))) = (P:'a. P(@x:'a. (P(x))))
