Theorem: Cpdt.Chapter2.Prog.denote_nil (Cpdt/Chapter2/Lang.lean)

State before:
s : Stack
⊢ denote [] s = some s
Tactic:
rfl
State after:
no goals