Having taken a quick look, I think I understand in part the concern by Sozeau and Timany, but I’m not fully convinced; indeed, as it is normal, neither proof fully covers Coq termination checking.

And according to them, the use of choice is unrelated to this point: they avoid the issue with Lee and Werner by proving consistency of a *different* system.

- Sozeau and Timany assumes that source programs are written using eliminators (that is, recursion is expressed by calling functions similar to Coq’s generated induction principles). However, Coq programs are written using recursive functions — as they point out, Coq programs need to be
*translated* to use eliminators.
- Lee and Werner assume they can perform termination checking by inspecting bodies of recursive functions. However, their rules are not applicable to Coq as-is: Coq normalizes function bodies before performing termination checking. If it didn’t, many Coq programs would be rejected and would have to be modified. Lee and Werner do not discuss this normalization step, and Sozeau and Timany appear to consider it unavoidable — and they demand proof that it terminates.

However, that seems debatable for various reasons.

- Other termination checkers, like Agda’s, do
*not* normalize functions before termination checking (however, this choice is a real problem in some cases, even tho Agda’s termination checker is more flexible in other ways).
- If one relies on Lee and Werner
*and* has the typechecker normalize functions before termination checking *and* strong normalization fails, the worst case seems a loop *during typechecking*, which does not endanger consistency. At worst, the user will interrupt typechecking and modify the program — which is often necessary anyway when using Coq.
- Last, Sozeau and Timany assume Coq programs have already been translated to use eliminators. Can that be done
*without* the problematic normalization? How?

Here’s the key paragraph from Timany and Sozeau (emphasis mine):

On the other hand, the occurrences of recursive calls in recursive functions are may be hidden under some computations. That is, **in order to obtain the position and arguments of recursive calls**, which are crucial for constructing the model of recursive functions, **in general requires normalizing the body of the recursive function.** It so appears that the intention of Lee and Werner [2011] is to construct a set theoretic model for Coq, assuming the normalization property which already implies soundness of their system.