Use [Admitted] rather than [admit] for axioms.

The newer versions of HoTT/coq support polymorphic axioms, and no longer
require the [admit] exploit.  This way, we have two fewer top-level
constants floating around.