Recherche:

La propriété que tu veux utiliser (s'il existe et est unique, je peux le construire) est "l'axiome de choix unique". Il existe dans la bibliothèque standard Coq Logic.ChoiceFacts sous les noms "AC!",...

Ce n'est pas parce qu'un élément existe et est unique que tu peux le construire.

Si tu considères que ton "existe" est constructif, tu peux extraire le témoin dans tous les cas; c'est exactement...

Disclaimer : je ne connais qu'assez mal Coq, et je manque beaucoup de pratique. À prendre avec des pincettes, donc.

Il me semble qu'en Coq, ce qui vit dans Set est intrinsèquement calculable et ce...