proposition: Lemma SameADTs_pop_SCA: forall (av : Type) (st : StringMap.t (Value av)) (k : StringMap.key) (v : W) ext, not_mapsto_adt k st = true -> SameADTs ext st -> SameADTs ext ([k |> wrap v]::st).
proof: Proof. eauto using SameADTs_Trans, SameADTs_pop_SCA_util. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas