Pour la preuve de programmes en Coq, qu'apporte concrètement la contrainte de ne pas utiliser le tiers-exclu (dans Prop ; dans Set je comprends parfaitement), l'égalité extensionnelle et l'indifférence à la preuve ?