proposition: Lemma set_ext : forall E F, (forall (x:A), x \in E <-> x \in F) -> E = F.
proof: Proof. Proof using. intros. rewrite~ set_ext_eq. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)