Coqの仕様なんでなんとも……
>>520でコラッツの定義としては問題ないと思います。