(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
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
)))
By:
GenDC (lem({
x
:
'a
|
P
(
x
) }))
Generated subgoals:
1
5.
x2
: {
x
:
'a
|
P
(
x
) }
P
(
x2
)
1
step
2
5. {
x
:
'a
|
P
(
x
) }
Void
P
(arb(
'a
))
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc
Prop
P(InjCase(lem({x:'a| P(x) }); x. x, arb('a)))
