proposition: Lemma ex_iff_Proper {A} : Proper (pointwise_relation _ iff ==> iff) (@ex A).
proof: Proof. lazy. intros ?? H; repeat (intros [] || intro || esplit); apply H; eassumption. Defined.
imports: Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Program.Basics Fiat.Common.Coq__8_4__8_5__Compat