(4steps total)
PrintForm
Definitions
Lemmas
hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq
pred
abstraction
2
1.
'a
: Type
2.
P
: (
'a
'a
)
Prop
3.
f
:eq(
'a
).
P
(
f
)
P
(
x
:
'a
.
y
:
'a
.
x
=
y
)
By:
InstHyp [
x
:
'a
.
y
:
'a
.
x
=
y
] 3 THEN StrongAuto
Generated subgoal:
1
(
x
:
'a
.
y
:
'a
.
x
=
y
)
eq(
'a
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
hol
Sections
HOLlib
Doc
'a
)
f:eq('a). P(f)
P(
x:'a. 
y)
eq('a)
