(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
1
1.
'a
: S
arb(
'a
) = (@
x
:
'a
. true
)
By:
Unab [`bchoose`] THEN Simp THEN StrongAuto
Generated subgoal:
1
arb(
'a
) = (@
x
:
'a
. True)
11
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
arb('a) = (@
x:'a. true
) arb('a) = (@x:'a. true) arb('a) = (@x:'a. True)
