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