(8steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
choose
elim
neg
1
1
1.
'a
: S
2.
P
:
'a
Prop
3.
Q
:
'a
Prop
4.
x
:
'a
.
Q
(
x
)
P
(
x
)
5. (
x
:
'a
.
Q
(
x
))
(
x
:
'a
.
P
(
x
))
6.
x
: {
x
:
'a
|
Q
(
x
) }
P
(
x
)
By:
AddEMHyp THEN Analyze 6 THEN StrongAuto
Generated subgoal:
1
6.
x
:
'a
7.
Q
(
x
)
8. XM
P
(
x
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc
Prop
x:'a. Q(x) 
P(x)
Q(x)) 
P(x)
