Edit TL;DR: Lean4 有 Definitional proof irrelevance，所以本篇内容纯瞎搞。不过还有一部分没瞎搞的，所以留着。 --- 上上次被 Heterogeneou...