(3steps total)
PrintForm
Definitions
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
lelt
int
vs
lelt
i
,
j
,
k
:
.
i
j
<
k
i
j
<
k
By:
Def of <
>
<
> <
<
> THEN UnivCD
Generated subgoal:
1
1.
i
:
2.
j
:
3.
k
:
((
i
j
)
(
j
<
k
))
i
j
<
k
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
FTA
Sections
DiscrMathExt
Doc