统一术语

[OlingCat]

依赖类型 -> 依值类型（Dependent Type）
英文为了简短会把 type depends on a value（依值而存的类型）缩减为
dependent type，中文还是两个字，因此可将缺失的宾语「值」补足。

析构 -> 解构（Destruct）
目前术语「析构」常用于 C++ 中的「析构函数」，本质是资源回收函数。
它的涵义和「构造」对应的「解构」完全不同，因此直接译作「解构」即可。
「构造子」对应「解构子」，不再译作「解构器」。

进行性 -> 可进性(Progress)
「进行」通常表示一种正在进行的状态，而书中表示的是一个项可进一步规约，
因此译作「可进性」。