(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
1.
'a
: S
arb(
'a
) = (@
x
:
'a
. True)
By:
Unab [`choose`] THEN StrongAuto
Generated subgoal:
1
arb(
'a
) = InjCase(lem({
x
:
'a
| True });
x
.
x
, arb(
'a
))
10
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) = InjCase(lem({x:'a| True }); x. x, arb('a))
