(5steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
choose
true
'a
:Type,
P
:(
'a
Prop),
x
:
'a
.
P
(
x
)
P
(@
x
:
'a
.
P
(
x
))
By:
Unfold `choose` 0
Generated subgoal:
1
1.
'a
: Type
2.
P
:
'a
Prop
3.
x
:
'a
4.
P
(
x
)
P
(InjCase(lem({
x
:
'a
|
P
(
x
) });
x
.
x
, arb(
'a
)))
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc
'a:Type, P:('a
Prop), x:'a. P(x) 
P(@x:'a. P(x)) 'a:Type, P:('aProp), x:'a. P(x) P(@x:'a. P(x))Prop
P(InjCase(lem({x:'a| P(x) }); x. x, arb('a)))
