The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

On 23 April 2014 11:17, AUGER Cédric <sedrikov AT gmail.com> wrote:

If you can decide of some property, then you have a form of irrelevance.
Any function to the 'bool' type can be converted in a function to
'Prop' by composition with 'conv (fun x => if x then True else False) :
bool -> Prop'. And for any boolean 'b', a term of type 'conv b' is
"irrelevant" (there is only a single habitant to that type).

That is mainly the main reason why we have UIP on decidable equalities.

This is, however, not sufficient for the trick I mentioned which needs conversion-level irrelevance. Which, indeed, isn't implemented in the current Coq. So, unfortunately, there is no conversion-level associativity yet in Coq. But we can hope the future makes it available.