(7steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hforall
def
1
1.
'a
: S
(
p
:
'a
.
x
:
'a
. (
p
(
x
))) = (
P
:
'a
.
P
=
(
x
:
'a
. true
))
By:
Simpset [`ext`] THEN StrongAuto
Generated subgoal:
1
2.
P
:
'a
(
p
:
'a
.
x
:
'a
. (
p
(
x
)))(
P
) = (
P
=
(
x
:
'a
. true
))
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
(
p:'a
. 
x:'a. (p(x))) = (P:'a. P = (x:'a. true
)) (p:'a. x:'a. (p(x))) = (P:'a. P = (x:'a. true))
(p:'a. x:'a. (p(x)))(P) = (P = (x:'a. true))
