Despite nominal techniques have stood the test of time, no nominal framework has been proposed for the Coq proof assistant. A work in progress formalization of nominal sets in Coq is presented, highlighting the main design decisions. Type classes and generalized rewriting mechanisms, also known as setoid rewriting, allows concise definitions and proofs, whilst avoiding the well-known “setoid hell” scenario. The present work is a first step for a nominal package for Coq.