在《赋型唯一性的证明过程简介》 提及到，κ 简化 （κ reduction）概念的引入，是为了证明，在不考虑 证据不区分（Proof Irrelevance）的情况，表达式具备唯一常态（Unique normal form），这使得 Church-Rosser 定理 得以证明，从而证明 n-provability是定义上方向（Definitional Inversion），最终，证明 赋型唯一性（Unique Typing）。
一、简化规则回顾
κ 简化 （κ reduction），可以简单地看作 β δ ζ ι 简化的统称。先回顾一下LEAN定义的简化规则，有：
β 简化（beta reduction）：
δ 简化（Delta reduction）：
ζ 简化（Zeta reduction）：
ι 简化（Iota reduction）：
另有，不属于 K 简化的 η 简化，（ Eta reduction）：
二、简化规则的选择 与 rec 常态 （rec-normal form）
通过对相等类型（Equality Type）使用函数的简化，来体现LEAN是如何规范简化规则的选择的。有：
相等类型（Equality Type）定义:
相等类型的使用函数（Recursor of Equality Type）:
其中：
动机函数（Motive function） C : (a: α) → {eqₐ a} → Uᵤ
次要函数组（Minors） C a：Uᵤ
主要作用对象（major）∀b: a = b
结果 C b：Uᵤ
那么，对于 表达式
λh:a = a. recₐ₌ C e a h ，
即，给入 a = a 的证明 h，输出结果 e。
但此时，有两种计算方式（Reduction）可以选择，即 η 简化（eta reduction）和 ι 简化（iota reduction）。有：
其中，在做 η 简化（eta reduction）后，表达式 为 recₐ₌ C e a，与含义不符。这就要求LEAN在选择计算规则是，需要约束其只能选择体现原含义的计算规则。即，LEAN 要求 使用函数 rec 的参数个数必须得到满足，即表达式 recₐ₌ C e a 不被允许，因此，表达式 λh:a = a. recₐ₌ C e a h 只能选 ι 简化（iota reduction）。
下图是LEAN 对简化规则使用的正式说明：
注：商类型（Quotient Type）的使用函数 lift 在 介绍 商类型（Quotient Type）时提及过，后续会有文章，进行详细讨论。
其中，第一点说明了，当 使用函数 rec 后跟着的参数个数少于其要求的参数个数是，其表达式的形态为 λx :: α. rec e x，即，上述的 recₐ₌ C e a ，不允许存在。
第三点说明，如果满足参数个数的要求，会先使用 η 简化（eta reduction），也叫 η 扩展（eta expanse），这个就是等式的解析，从左到右看或从右到左看了。
此时，满足 rec 参数要求的表达式，称为 rec 常态 （rec-normal form）。
三、rec 常态 （rec-normal form）的属性
四、K 简化（K Reduction）定义
其实，就是将把 β δ ζ ι 简化 定义在 rec-normal form 上，统称为 K 简化（K Reduction）。
五、证据不区分（Proof Relevance）关系
证据不区分（Proof Relevance）会导致 表达式没有唯一的常态，但是，如果两个表达式间有证据不区分（Proof Relevance）关系，那么，实际意义上，两表达式是定义上相等的。由此，通过下面定义指示，两个表达式在证据不区分（Proof Relevance）的情况下，定义上相等（Definitional Equal），记，≡ₚ ，即 对于具备证据不区分（Proof Relevance）关系的两表达式的简化规则（Reduction Rule）。
上述 ≡ₚ 定义的推演规则，说明，如果表达式中带有 p: P，那么基于证据不区分（Proof Relevance），其形变应遵从 ≡ₚ 定义的推演规则。
六、小结
至此，简化规则就包括 K简化（K Reduction）和 针对具备证据不区分（Proof Relevance）关系的简化规则，具备后续推导 Church-Rosser 定理 的准备。另外，简化规则有下面属性：
