Remove eqtype declaration for term type

Fix arithmetic d.p. mis-feature identified in c59783a4d0e3d

Issue was that conditional expressions with non-presburger guards
resulted in goals that weren't provable because ARITH couldn't handle
boolean sub-terms that weren't presburger. This prevented its
instance-generalisation mechanism from solving obvious goals like that
in the test-case.

Now the instance-generalisation mechanism will perform up to four
case-splits on boolean sub-terms. Of course, the choice of four is
completely arbitrary, but a possible 32-fold expansion in goal-size
seems unreasonable.

Document the change in the release notes.

Minor bugfix Bug arose from moving to Kan. 0.
Also shifting library to use numSyntax.

Directory now Kananaskis compatible, though no real testing done.
Loads of warnings about illegal style.

Change to structure of numLib so that reduce and arith are incorporated.