Theorem: Cpdt.Chapter2.TExp.concat_correct (Cpdt/Chapter2/Typed.lean)

State before:
ts1 ts2 ts3 : TStack
⊢ ∀ (p1 : TProg ts1 ts2) (p2 : TProg ts2 ts3) (s : VStack ts1),
    TProg.denote (concat p1 p2) s = TProg.denote p2 (TProg.denote p1 s)
Tactic:
intro p1
State after:
ts1 ts2 ts3 : TStack
p1 : TProg ts1 ts2
⊢ ∀ (p2 : TProg ts2 ts3) (s : VStack ts1), TProg.denote (concat p1 p2) s = TProg.denote p2 (TProg.denote p1 s)

State before:
ts1 ts2 ts3 : TStack
p1 : TProg ts1 ts2
⊢ ∀ (p2 : TProg ts2 ts3) (s : VStack ts1), TProg.denote (concat p1 p2) s = TProg.denote p2 (TProg.denote p1 s)
Tactic:
induction p1 <;> simp_all
State after:
no goals