proposition: Lemma eq_union_single_remove_one : forall E x, x \in E -> E = \{x} \u (E \-- x).
proof: Proof. Proof using. introv H. set_unf. extens. intros y. iff M. simpls. tests*: (y = x). destruct M. subst*. autos*. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)