proposition: Lemma not_mapsto_adt_eq_SCA: forall (av : Type) (k : StringMap.key) (w : W) (fmap : StringMap.t (Value av)), not_mapsto_adt k (StringMap.add k (SCA av w) fmap) = true.
proof: Proof. eauto using MapsTo_SCA_not_mapsto_adt, StringMap.add_1. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas