1階命題論理でresolutionが成り立つ事を示す

まずAかBかで場合を分けて、Aのときは¬AかCかで場合分けすればできる。Aと¬Aが同時に成り立つとなんでも証明できてしまうということを利用しよう。排中律は別に必要なく証明できる。

Proposition p09 :
  forall A B C, (A \/ B) /\ (~A \/ C) -> B \/ C.
Proof.
intros A B C H; elim H; intros.
elim H0.
 elim H1.
  intros H2 H3; elim H2.
    apply H3.
 intros H2 _; right; apply H2.
intro H2; left; apply H2.
Qed.