Definition toto := Set.
Definition toto := Set.