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