(5steps total)
PrintForm
Definitions
hol
arithmetic
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hless
or
eq
all(
m
:hnum. all(
n
:hnum. equal(le(
m
,
n
),or(lt(
m
,
n
),equal(
m
,
n
)))))
By:
HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))
Generated subgoal:
1
1.
m
:
2.
n
:
(
m
n
) = (
m
<
n
(
m
=
n
))
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
hol
arithmetic
2
Sections
HOLlib
Doc