Como definir conjunto em coq sem definir conjunto como uma lista de elementos
Eu estou tentando definir (1,2,3) como um conjunto de elementos em coq. Eu posso defini-lo usando list como (1 :: (2 :: (3 :: nil))). Existe alguma maneira de definir conjunto no coq sem usar a lista.