Почему программа проверки завершения Coq не поддерживает случай, когда один аргумент становится структурно меньше, а другие остаются прежними

Программа проверки завершения Coq не любит такие функции, как:

Fixpoint interleave (A : Type) (l1 l2 : list A) : list A :=
  match l1 with 
  | cons h1 t1 => cons h1 (interleave l2 t1)
  | nil => l2
  end.

Однако некоторые другие языки с аналогичными средствами проверки завершения, такие как Lean, Idris и Isabelle, принимают такие функции. Мне интересно, почему средство проверки завершения Coq не принимает такие функции, когда по крайней мере один аргумент становится структурно меньше каждый раз, а аргументы не становятся больше. Мне кажется, что если хотя бы один аргумент всегда становится меньше и ни один не растет, функция должна в конечном итоге завершиться, или есть какой-то случай, который мне не хватает?

Edit: Кажется, я выбрал ужасный пример, поскольку, очевидно, Идрис и Лин тоже не могут с этим справиться. Лучшим примером может служить формулировка «исправление в исправлении», приведенная в Как работать с действительно большими терминами, созданными программой Fixpoint в Coq?; Я знаю, что мне удалось реализовать ту же функцию в Lean и Idris напрямую, не требуя конструкции «исправление в исправлении». Кроме того, остается открытым исходный вопрос: почему эта конструкция не поддерживается?