Theorem: Cpdt.Chapter2.Prog.denote_iBinop_nil (Cpdt/Chapter2/Lang.lean)

State before:
p : Prog
op : Binop
⊢ denote (Instr.iBinop op :: p) [] = none
Tactic:
rfl
State after:
no goals