coq_practice_21_(1,2).v

(* 必要な公理を入れる *)
Require Import Coq.Logic.Classical.
Lemma ABC_iff_iff :
    forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
  intros.
  tauto.
Qed.

(* 必要な公理を入れる *)

Goal
  forall P Q R : Prop,
  (IF P then Q else R) ->
  exists b : bool,
  (if b then Q else R).
Proof.
  intros.
  destruct H.
    exists true.
    destruct H.
    apply H0.
  
    exists false.
    destruct H.
    apply H0.
Qed.