fix和cofix的终止检查是它们良好形式性规则的一部分。如果我们忽略了这一点，那么这些构造的另一个重要区别特征就是计算规则。
用不同的措辞来表达这个问题：如果我们分别取消对归纳和共导数据类型的使用的终止检查和保护性条件，那么归纳/共导和修复/共修复之间会不再有根本区别吗？
通过"；基本差异"；我指的是Coq核心演算的差异，而不是语法和证明搜索等方面的差异。
这似乎最终归结为一个关于构造微积分的问题。
注意：我知道一个定理证明者，跳过终止检查/递归的安全性/共诅咒可以证明False——所以，如果它有帮助，请把它当作一个关于非完全编程的问题，而不是证明。
fix只有当其递减参数是构造函数时才递减cofix仅在析构函数(match或基元投影(下减少
(* stuck *)
(fix f x {struct x} := body f x)
(* not stuck *)
(fix f x {struct x} := body f x) (S y)
=
body (fix f x := body f x) (S y)
(* stuck *)
(cofix g x := body g x)
(* not stuck *)
match (cofix g x := body g x) with _ => _ end
= match body (cofix g x := body g x) x with _ => _ end
这些特殊的规则就是为了确保终止合同。如果你不在乎这一点，并允许fix和cofix在任何上下文中展开，那么它们的行为与不动点组合子相同：
(fix f x := body f x)
=
(fun x => body (fix f x := body f x) x)
(cofix g x := body g x)
=
(fun x => body (cofix g x := body g x) x)