由于定义上相等（Definitional Equality）作用在所有情况，由此，当遇到不一致（Inconsistent）的时候，会导致其结果是不确定的，即会无限展开（unfolding forever）下去。
原文中，是通过一个定义在自然数（ℕ）的大于关系（>）上的可达类型（Accessibility Type）来论证，这个看原文很好理解，这里就不再赘述了。
关键点：要证明 acc x，x ∈ℕ，那么所有，r y x 的 y 都是 acc y，r ≡ >，即 y > x。由此，在自然数中，有无数个比 x 大的自然数，这样导致不能证明 acc x。如果给定一个 a，其类型为 acc x，那么，在使用该 a: acc x 时，就会对 a 进行无限地展开（unfolding），导致无法停止（Non-terminated）。
下面列出其证明过程：
函数 f 的类型：f : (n: ℕ) → Acc n → 1， 且，1 ≡ Unit， （）：Unit，即 （）：1.
其中函数 g: ∀y.y>x → 1 ≡ (y: ℕ) → h: (y>x) → 1，意思是，给定一个自然数 y，以及，证明 y > x，那么，该函数就会返回 ()。也就是说，当无法给入 g 的输入参数时，是无法调用 g 的。
另外，函数 g，是在可达类型的使用规则里，给定的，表示使用规则中的前果。因此，根据 可达类型的使用规则（Elimination Rule），即使用函数 rec，函数 g 为 前果，有
g (n + 1) (p n) ≡ f (n + 1) a
≡ f (n+1) (intro (inv a))
≡ f (n+1) (inv a (n + 1) (p n) )
≡ f (n+1) (h (n + 1) (p n) )
其中，h 为 ∀y.y>x → acc y 的证明（proof）。
由此，其步进规则，有
当 n = 0，a : Acc n，即 a : Acc 0，有 a ≡ intro (inv a) ，那么
因此
口
标签：Definitional,acc,Equality,函数,Acc,inv,自然数,LEAN,类型 From： https://blog.csdn.net/sinat_36821938/article/details/141960107