proposition: Lemma not_mapsto_adt_not_MapsTo_ADT : forall {av k st}, @not_mapsto_adt av k st = true -> forall {v: av}, not (StringMap.MapsTo k (ADT v) st).
proof: Proof. not_mapsto_adt_t; red; intros; not_mapsto_adt_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas