proposition: Lemma not_mapsto_adt_neq_remove: forall (av : Type) (s : string) (k : StringMap.key) (st : StringMap.t (Value av)), k <> s -> not_mapsto_adt k (StringMap.remove (elt:=Value av) s st) = true -> not_mapsto_adt k st = true.
proof: Proof. not_mapsto_adt_t; SameValues_Facade_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas