Theorem double_negation_elim : forall A : Prop, ~~A -> A.
Proof.
  unfold not.
  intros A H.
  (* stuck because no way to reach A with H : (A -> False) -> False *)
Abort.

Lemma not_not_lem: forall A: Prop, ~ ~(A / ~A).
Proof.
  intros A H.
  unfold not in H.
  apply H.
  right.
  intro a.
  destruct H.
  left.
  apply a.
Qed.

Theorem not_not_lem_implies_lem:
  (forall (A : Prop) , (~~A -> A)) -> forall A : Prop, A / ~A.
Proof.
  intros H A.
  apply H.
  apply not_not_lem.
Qed.