The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

As Enrico and Xavier pointed out, convertible terms are identical as
far as Coq is concerned.  It is "only" a heuristic question of what
paths to try through the extremely large space of conversion paths.
(Although, as Braibant points out, changing heuristics could (will)
break something that checks with the current heuristics.)

Furthermore it isn't just about unfolding definitions; a definition
folding, or a beta expansion, might make the difference between
infeasible and feasible conversion.

I don't know the answer, but I've always thought some notation system
for hints about conversion paths might be part of it.

Another idea is that once Coq has found a satisfactory conversion path
(possibly by backtracking), some hints about this path might be
included in the constructed proof term.