zoeyfyi

Require Import Coq.Classes.SetoidClass.

Program Instance Iff1Setoid{A:Type} : Setoid (A->Prop) := {|
  equiv := fun P Q => forall x, P x <-> Q x
|}.
Next Obligation.
  split.
  - intros P x; reflexivity.
  - intros P Q H x; symmetry; exact (H x).
  - intros P Q R H0 H1 x; transitivity (Q x); [exact (H0 x)|exact (H1 x)].