proposition: Lemma set_in_single_eq : forall x y, x \in (\{y}:set A) = (x = y).
proof: Proof. Proof using. apply in_single_eq. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)