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