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

State before:
a✝³ a✝² : TStack
i : TInstr a✝³ a✝²
a✝¹ : TStack
ps : TProg a✝² a✝¹
a✝ : TStack
rs : TProg a✝¹ a✝
⊢ concat (cons i ps) rs = cons i (concat ps rs)
Tactic:
rfl
State after:
no goals