LEAN 赋型唯一性（Unique Typing）之 在 n-provability 下 的 赋型唯一性

                《LEAN 赋型唯一性（Unique Typing）之 证明过程简介》 中，介绍到，在证明赋型唯一性（Unique Typing ）时，引入了 n-provability 的概念，通过证明在 n-provability 情况下的赋型唯一性，来证明系统的 赋型唯一性。此篇文章介绍在 n-provability 情况下的赋型唯一性。

        首先需要引入定义上反向（Definitional Inversion）的概念，类似于具备双射（Bijection）的函数，具备反向函数（Inverse Function），那样，以描述某些赋型规则具备类似双射（Bijection）的属性，也就是，说明了该赋型规则的因果唯一性。

一、定义上反向（Definitional Inversion）

对比对应的定义上相等规则，有

1. 

2.

3.

二、n-provability 上的赋型唯一性

有

将上述的第三点，对着对应的赋型规则来看，有

其中，类型α 的类型为 Uₗ₁, Uₗ₁'，即 α: Uₗ₁, Uₗ₁'， 同理有， β: Uₗ₂, Uₗ₂' 。

同时，因 归纳假设（Inductive Hypotheses），有 Uₗ₁ ≡ Uₗ₁' 和 Uₗ₂ ≡ Uₗ₂' 。

又因，定义上反向（Definitional Inversion），有 l₁ ≡ l₁' ， l₂ ≡ l₂' 。

因此，有

即， 

且，

        这个结论，可以为后续的赋型规则提供归纳假设（Inductive Hypotheses），以证明，赋型规则（Typing Rules）保持了（preserve）类型在定义上相等的关系。

        从上述论证过程，也能看出，定义上反向的作用，在某些赋型规则（Typing Rules）中，起作用，因此，需要证明其定义上反向（Defintional Inversion）的属性。

        另外，从上面的过程总结来看，其结构为，基于某一赋型规则，对于其前提中的赋型，由归纳假设（Inductive Hypotheses）来给定；其结论的赋型的定义上相等关系，由当前赋型规则及归纳假设来求证，使得，结论中的赋型，定义上相等。

        即， 其结构为

                归纳假设（Inductive Hypotheses）定义的两类型定义上相等，

                        如 α：Uₗ₁ ≡ Uₗ₁' 和 β：Uₗ₂ ≡ Uₗ₂'

                ⇒ 赋型规则（Typing Rule）

                ⇒ 结论中的两类型定义上相等 ，如 ∀x:α.β：Uimax(𝑙₁, 𝑙₂) ≡ Uimax(𝑙₁', 𝑙₂') 

        即，上述证明的第1点叙述的。其它两点，可基于上述内容自行理解。

        此时，已经能证明了，如果 n-provability 是定义上反向（Definitional inversion）的话，在 n-provability 上，LEAN具备赋型唯一性。那么，接下来需要证明的是，n-provability 是定义上反向（Definitional inversion）。

        通过证明 ⊢₀ 与 ⊢ₙ₊₁ 都具备定义上反向（Definitional inversion），那么  ⊢ₙ 具备定义上反向（Definitional inversion），即，n-provability 是定义上反向（Definitional inversion）。

        由此，后续的文章注解  ⊢₀ 与 ⊢ₙ₊₁ 都具备定义上反向（Definitional inversion）的证明。