Theorem: Cpdt.Chapter2.TExp.denote_nConst (Cpdt/Chapter2/Typed.lean)

State before:
n : Nat
⊢ denote (nConst n) = n
Tactic:
rfl
State after:
no goals