Recherche:

TropMDR : j'ai proposé cet axiome dans le but de modéliser l'opérateur de comparaison polymorphe de OCaml. C'est effectivement un mauvais conseil (... et un mauvais opérateur) si le but est de tout...

C'est bien, mais maintenant il faut prouver la correction :mur:

Ton erreur est de définir "Variable (C : Set)." puis "Hypothesis compare : C -> C -> order". Du coup C est une globale et tous les arguments passés à "compare" sont inférés de type C. Une imprudence...