Library basic

Require Import Coq.Program.Basics.
Require Export Setoid Morphisms Morphisms_Prop.

Lemma fa_mono : forall A (B B':A->Prop),
  (forall x, impl (B x) (B' x)) -> impl (forall x, B x) (forall x, B' x).

Lemma fa_morph : forall A (B B':A->Prop),
  (forall x, B x <-> B' x) -> ((forall x, B x) <-> (forall x, B' x)).

Instance ex_mono : forall A,
  Proper (pointwise_relation A impl ==> impl) (@ex A).
Qed.

Instance ex_morph : forall A,
  Proper (pointwise_relation A iff ==> iff) (@ex A).

Qed.

Instance ex2_mono : forall A,
  Proper (pointwise_relation A impl ==> pointwise_relation A impl ==> impl) (@ex2 A).
Qed.

Instance ex2_morph : forall A,
  Proper (pointwise_relation A iff ==> pointwise_relation A iff ==> iff) (@ex2 A).

Qed.

Lemma iff_morph : Proper (iff ==> iff ==> iff) iff.

Lemma iff_impl : forall A B, iff A B -> impl A B.