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

Generated subgoals:

None

About:
boolassertintequalall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas hol Sections HOLlib Doc