Agdaによる「プログラミング言語の基礎概念」 - 導出システムNatのメタ定理：Rainy Day Codings：So-net blog

第1章で定義した導出システムNatについてのメタ定理を証明していく。 module igarashi2 where open import Data.Nat using (ℕ; zero; suc) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; subst) open import Data.Product using (_×_; proj₁; proj₂; ∃-syntax) renaming (_,_ to ⟨_,_⟩) open import igarashi1 定理2.1 加算の単位元 定理2.1はゼロが加算の単位元であることを左右それぞれ証明する。 -- +-identityˡ theorem2-1-1 : ∀ {n : ℕ} ---------------- → NatJudg