proposition: Lemma eval_AssignVar_MapsTo: forall (av : Type) (var : StringMap.key) (val : W) (state : State av), StringMap.MapsTo var (SCA av val) state -> eval state (Var var) = Some (SCA av val).
proof: Proof. intros; apply find_mapsto_iff; assumption. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.PureUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.FacadeUtils Coq.Setoids.Setoid