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

State before:
a✝² a✝¹ : TStack
i : TInstr a✝² a✝¹
a✝ : TStack
p : TProg a✝¹ a✝
s : VStack a✝²
⊢ denote (cons i p) s = denote p (TInstr.denote i s)
Tactic:
rfl
State after:
no goals