proposition: Lemma is_true_eq_MapsTo : forall av st var val, is_true st (TestE IL.Eq (Var var) (Const val)) -> StringMap.MapsTo var (SCA av val) st.
proof: Proof. intros. unfold is_true, is_false, eval_bool, eval, eval_binop_m, eval_binop, IL.evalTest in *. repeat match goal with | _ => cleanup_pure | _ => cleanup_facade_pure; subst | _ => MoreStringMapFacts.normalize | [ H: context[StringMap.find ?k ?v] |- _ ] => destruct (StringMap.find k v) eqn:eq0 | [ H: context[IL.weqb ?a ?b] |- _ ] => destruct (IL.weqb a b) eqn:eq1 | [ H: Value _ |- _ ] => destruct H | [ H: _ = Some _ |- _ ] => compute in H end. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.PureUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.FacadeUtils Coq.Setoids.Setoid