rw [List.append_assoc (Exp.compile r)]
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ (Exp.compile l ++ [Instr.iBinop b]) ++ p) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
case binop
b : Binop
l r : Exp
lih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile l ++ p) s = Prog.denote p (Exp.denote l :: s)
rih : ∀ (p : Prog) (s : Stack), Prog.denote (Exp.compile r ++ p) s = Prog.denote p (Exp.denote r :: s)
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile r ++ (Exp.compile l ++ [Instr.iBinop b] ++ p)) s =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)