Make tests runnable again by removing some axioms.

For some reason, Coq's extractor chooses to evaluate axioms eagerly, which
triggers exceptions even if the axioms are actually unused...