Require Import List.

Require Import CpdtTactics.

Set Implicit Arguments.

(* don't use tauto *)

Section Propositional.
  Variables P Q R : Prop.

  Theorem contra : P -> ~P -> R.
  Admitted.

  Theorem and_assoc : (P /\ Q) /\ R -> P /\ (Q /\ R).
  Admitted.

  Theorem or_assoc : (P \/ Q) \/ R -> P \/ (Q \/ R).
  Admitted.

  Theorem uncurry : (P -> Q -> R) -> (P /\ Q -> R).
  Admitted.

  Theorem curry : (P /\ Q -> R) -> (P -> Q -> R).
   Admitted.

End Propositional.

Theorem forall_exists_commute : forall (A B : Type) (P : A -> B -> Prop),
  (exists x : A, forall y : B, P x y) -> (forall y : B, exists x : A, P x y).
  Admitted.