proposition: Lemma MapsTo_ADT_not_mapsto_adt_true: forall {av} (k : StringMap.key) (st : StringMap.t (Value av)) (a : av), StringMap.MapsTo k (ADT a) st -> not_mapsto_adt k st = false.
proof: Proof. not_mapsto_adt_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas