rw [Prog.denote_iBinop_2args]
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 (Instr.iBinop b :: p) (Exp.denote l :: Exp.denote r :: s) =
    Prog.denote p (Binop.denote b (Exp.denote l) (Exp.denote r) :: s)
no goals