(* exercise 4.3 from Coq Art *)

Lemma all_perm :
  forall (A : Type) (P : A -> A -> Prop),
    (forall x y : A, P x y) ->
      forall x y : A, P y x.
Proof.
  intros A P H x y.
  apply H.
Qed.

Lemma resolution :
  forall (A : Type) (P Q R S : A -> Prop),
    (forall a : A, Q a -> R a -> S a) ->
      (forall b : A, P b -> Q b) ->
        forall c : A, P c -> R c -> S c.
Proof.
  intros A P Q R S H H0 c H1 H2.
  apply H; try assumption.
  apply H0; assumption.
Qed.