proposition: Lemma NotIn_not_mapsto_adt : forall {av} var (state: StringMap.t (Value av)), var ∉ state -> not_mapsto_adt var state = true.
proof: Proof. unfold not_mapsto_adt, is_mapsto_adt, is_some_p; intros. rewrite not_in_find; tauto. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.PureUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.FacadeUtils Coq.Setoids.Setoid