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.
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.