Rocq uses an algorithm with heuristics to test convertibility of terms. While these heuristics work fine for many problems, some simple convertibility problems can take forever. Usually, these problems are between convertible terms obtained using a reduction tactic. We propose to add a convertibility checker that takes a convertibility certificate to speed up convertibility checks in such cases.
