alphabetise the order of the inferences in proves_rules
tweak context_ok, and take it more seriously

use context_ok in the definition of entails...
fix most soundness proofs and attempt more of new_specification

But the proof of new_specification does not look promising: it seems
like the subgoal I got to is probably false, because it wants the new
constant to have the same semantics as the witness term. I must have
made a too specific choice somewhere in the proof...?