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