Coq演習

17.v

Theorem hoge : forall P Q R : Prop, P \/ ~(Q \/ R) -> (P \/ ~Q) /\ (P \/ ~R).
Proof.
  refine (fun P Q R H => _).
  refine (match H with
              | or_introl HP => _
              | or_intror  HnQR => _
          end).
  - exact (conj (or_introl HP) (or_introl HP)).
  - refine (conj _ _).
    + refine (or_intror (fun HQ => _)).
      exact (HnQR (or_introl HQ)).
    + refine (or_intror (fun HQ => _)).
      exact (HnQR (or_intror HQ)).
Qed.