(7steps total)
PrintForm
Definitions
Lemmas
hol
bool
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hexists
def
1
1
1
1.
'a
: S
2.
P
:
'a
(
x
:
'a
. (
P
(
x
))) =
P
(@
x
:
'a
. (
P
(
x
)))
By:
Simpset [`bequal`] THEN Simp THEN StrongAuto
Generated subgoals:
1
3.
x
:
'a
.
P
(
x
)
P
(@
x
:
'a
. (
P
(
x
)))
2
steps
2
3.
P
(@
x
:
'a
. (
P
(
x
)))
x
:
'a
.
P
(
x
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
hol
bool
Sections
HOLlib
Doc
(
x:'a. (P(x))) = P(@x:'a. (P(x)))
(x:'a. (P(x))) = P(@x:'a. (P(x)))x:'a. P(x)
P(@x:'a. (P(x)))
x:'a. (P(x)))
x:'a. P(x)
