(* Exercise 31 *)

Require Import BenB.

(*Variable D : Set.*)
Definition D:= R.
Variables P Q S T : D -> Prop.
Variable R : D -> D -> Prop.

Theorem exercise_031 :
  (forall x:D, P x /\ Q x)
->
  (forall x:D, P x \/ exists y:D, R x y).
Proof.
imp_i ass1.
all_i t.
dis_i1.
con_e1 (Q t).
all_e (forall x : D, P x /\ Q x) t.
hyp ass1.
Qed.