直観主義論理での二重否定除去と排中律の同値性

同値性を示すためにそれぞれの矢印を示した。論理パズルみたいな問題だが、¬を扱ういい練習問題だと思う。

Lemma p10_left :
  (forall A, ~~A -> A) -> (forall A B, (~B -> ~A) -> (A -> B)).
Proof.
intros.
apply H.
intro.
elim (H0 H2).
apply H1.
Qed.

Lemma p10_right :
  (forall A B, (~B -> ~A) -> (A -> B)) -> (forall A, ~~A -> A).
Proof.
intros.
apply (H True A).
 intro.
   intro.
   elim H0.
   apply H1.
apply I.
Qed.