replace WithK with a file in Axiom containing statement and consequences of UIP/K

[ecavallo]

Resolves #830. This way we don't have a file that relies on an extra flag and isn't usable in the rest of the library (and needs its own special case in the Makefile).