proposition: Lemma SameSCAs_pop_SCA: forall (av : Type) (st : StringMap.t (Value av)) (k : StringMap.key) (ext : StringMap.t (Value av)) (v : W), k ∉ st -> SameSCAs ext st -> SameSCAs ext ([k |> wrap v]::st).
proof: Proof. eauto using SameSCAs_Trans, SameSCAs_pop_SCA_util. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas