Cómo definir set en coq sin definir set como una lista de elementos
Estoy tratando de definir (1,2,3) como un conjunto de elementos en coq. Puedo definirlo usando list como (1 :: (2 :: (3 :: nil))). ¿Hay alguna manera de definir el conjunto en coq sin usar la lista?