proposition: Lemma SameSCAs_pop_SCA_util: forall (av : Type) (st : StringMap.t (Value av)) (k : StringMap.key) (v : W), k ∉ st -> SameSCAs st ([k |> wrap v]::st).
proof: Proof. unfold SameSCAs; intros; map_iff; match goal with | [ k: StringMap.key, k': StringMap.key |- _ ] => destruct (StringMap.E.eq_dec k k'); subst end; SameValues_Facade_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas