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

State before:
t : Ty
⊢ ∀ (e : TExp t) (ts : TStack) (s : VStack ts), TProg.denote (compile e ts) s = (denote e, s)
Tactic:
intro e
State after:
t : Ty
e : TExp t
⊢ ∀ (ts : TStack) (s : VStack ts), TProg.denote (compile e ts) s = (denote e, s)

State before:
t : Ty
e : TExp t
⊢ ∀ (ts : TStack) (s : VStack ts), TProg.denote (compile e ts) s = (denote e, s)
Tactic:
induction e <;> simp_all[compile, concat_correct]
State after:
no goals