proposition: Lemma not_mapsto_adt_remove : forall (av : Type) (s : string) (k : StringMap.key) (st : StringMap.t (Value av)), not_mapsto_adt k st = true -> not_mapsto_adt k (StringMap.remove s st) = true.
proof: Proof. intros. not_mapsto_adt_t. match goal with | [ H: StringMap.MapsTo ?k (ADT ?v) ?m |- _ ] => learn (MapsTo_ADT_not_mapsto_adt_true H2) end. congruence. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas