proposition: Lemma not_mapsto_adt_neq_remove' : forall {av} (s : string) (k : StringMap.key) v (st : StringMap.t (Value av)), k <> s -> not_mapsto_adt k st = true -> not_mapsto_adt k (StringMap.add s v st) = true.
proof: Proof. not_mapsto_adt_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas