Lorsqu'en Coq, on a une propriété à définir sur un type inductif T, faut-il mieux définir une fonction T->Prop par point fixe, ou définir un prédicat inductif T->Prop? Le premier cas n'est évidemment pas applicable si la décision du cas à appliquer n'est pas (quasi) déterministe en fonction du constructeur de T rencontré à la racine. Le second cas oblige à utiliser des inversions, qui peuvent parfois poser problème.

Sylvain Boulmé me suggère de faire les deux en démontrant une équivalence... D'ailleurs, est-ce que ça marche bien, la réécriture Setoid par l'équivalence logique ? Je l'ai utilisée sur quelques exemples, mais y a-t-il des problèmes cachés ? Est-ce fondamentalement plus complexe ou piège que la réécriture par l'égalité de Leibniz ?