PrintForm
Definitions
Lemmas
hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
not
lt
int
i
,
j
:
.
i
<
j
j
i
By:
RewriteOfThm Thm*
i
,
j
:
.
i
<
j
= (
j
i
) (SimpsetC [`bequal`]) THEN Id
THEN
Simp
THEN
StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
hol
Sections
HOLlib
Doc
i,j:
. 
i<
j 
j
i i,j:. i<j jii,j:. i<j = (ji) (SimpsetC [`bequal`]) THEN Id
