Fix an indentation glitch
Fix & document an infinite loop bug in intSimps.{OMEGA,COOPER}_ss

Problem was that the term F was viewed as suitable context for the
simplifier's decision procedure. Though superficially reasonable, this
leads to problems because the simplifier will rewrite everything it
can inside this context to F, using the rewrite

    [F] |- somegenvar = F          (1)

but the integer decision procedures will correctly rewrite occurrences
of F to T, because the underlying conversion is happy to prove

    |- (F ==> F) <=> T

The natural number procedure in ARITH_ss doesn't suffer from this
problem because it doesn't add F as context to the decision
procedure's context, and that's the fix taken here.

The decision to use (1) above rather than rewrite to true, say, was
taken in 9bc4bdaa.