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

State before:
a✝¹ a✝ : TStack
ps : TProg a✝¹ a✝
⊢ concat nil ps = ps
Tactic:
rfl
State after:
no goals