proposition: Lemma not_mapsto_adt_add: forall av (k k' : StringMap.key) v (fmap: _ (_ av)), k <> k' -> not_mapsto_adt k (StringMap.add k' v fmap) = not_mapsto_adt k fmap.
proof: Proof. intros. unfold not_mapsto_adt, is_mapsto_adt, is_some_p. rewrite add_neq_o by congruence. reflexivity. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.PureUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.FacadeUtils Coq.Setoids.Setoid