proposition: Lemma CompileBinopOrTest_right_inPlace: forall {av} op name var2 (val1 val2: W) env ext (tenv: Telescope av), name ∉ ext -> NotInTelescope name tenv -> StringMap.MapsTo var2 (wrap val2) ext -> {{ [[`name ->> val1 as _]]::tenv }} (Assign name (WrapOpInExpr op (Var name) (Var var2))) {{ [[`name ->> (eval_binop op val1 val2) as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. destruct op; SameValues_Facade_t. Qed.
imports: CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics