Axiom proof_admitted : False.
Ltac admit := case proof_admitted.