直観主義論理での二重否定除去と排中律の同値性
同値性を示すためにそれぞれの矢印を示した。論理パズルみたいな問題だが、¬を扱ういい練習問題だと思う。
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.