coercion-invariant arguments at work

constants with coercion-invariant arguments (possibility to disable/reenable coercions under certain constants, necessary for the forthcoming logically unspecified control structures for case translations)

simplified Proof.future_proof;

provide explicit dummy names (cf. dfe469293eb4);

discontinued empty name bindings in 'axiomatization';

provide common HOLogic.conj_conv and HOLogic.eq_conv;