(2steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
add
eq
pred
qf
'a
:Type,
P
:Prop.
P
(
f
:eq(
'a
).
P
)
By:
Id THEN StrongAuto THEN Try (Complete (Unfold `label` 0))
Generated subgoal:
1
1.
'a
: Type
2.
P
: Prop
3.
f
:eq(
'a
).
P
P
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc
'a:Type, P:Prop. P 
(f:eq('a). P) 'a:Type, P:Prop. P (f:eq('a). P)f:eq('a). P
P
