Double negation elimination

dne.v

Axiom a1 : forall A B, A -> (B -> A).
Axiom a2 : forall A B, (~B -> ~A) -> (A -> B).

Theorem dne :
  forall A, ~~A -> A.
Proof.
  intros A P.
  generalize P.
  apply a2, a2, a1, P.
Qed.

Print dne.
(*
dne = 
fun (A : Prop) (P : ~ ~ A) =>
a2 (~ ~ A) A
  (a2 (~ A) (~ ~ ~ A)
     (a1 (~ ~ A) (~ ~ ~ ~ A) P)) P
     : forall A : Prop, ~ ~ A -> A

Argument scopes are [type_scope _]
*)