Theorem: Cpdt.Chapter2.TProg.denote_nil (Cpdt/Chapter2/Typed.lean)

State before:
a✝ : TStack
s : VStack a✝
⊢ denote nil s = s
Tactic:
rfl
State after:
no goals