(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
1
1.
i
:
2.
j
:
3.
k
:
((
i
j
)
(
j
<
k
))
i
j
<
k
By:
RW bool_to_propC 0
Generated subgoal:
1
i
j
&
j
<
k
i
j
<
k
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
FTA
Sections
DiscrMathExt
Doc