proposition: Lemma eval_Binop_Some: forall (av : Type) (var1 var2 : StringMap.key) (val1 val2 : W) (ext : StringMap.t (Value av)) op (H1 : StringMap.MapsTo var2 (SCA av val2) ext) (H0 : StringMap.MapsTo var1 (SCA av val1) ext), eval ext (Binop op (Var var1) (Var var2)) = Some (SCA av (eval_binop (inl op) val1 val2)).
proof: Proof. intros; rewrite find_mapsto_iff in *; unfold eval, eval_binop_m; repeat match goal with | [ H: ?a = ?b |- context[?a] ] => rewrite H end; reflexivity. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.PureUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.FacadeUtils Coq.Setoids.Setoid