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

State before:
t : Ty
⊢ ∀ (e : TExp t), TProg.denote (compile e []) () = (denote e, ())
Tactic:
simp [compile_correct_helper]
State after:
no goals