(13steps total)
PrintForm
Definitions
Lemmas
hol
restr
binder
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
harb
wd
'a
:S. equal(arb,select(
x
:
'a
. t))
By:
Simpsetp [`hol_to_nuprl`] THEN StrongAuto
Generated subgoal:
1
1.
'a
: S
arb(
'a
) = (@
x
:
'a
. true
)
12
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(13steps total)
PrintForm
Definitions
Lemmas
hol
restr
binder
Sections
HOLlib
Doc
'a:S. equal(arb,select(
x:'a. t)) 'a:S. equal(arb,select(x:'a. t)) arb('a) = (@
x:'a. true
)
