proposition: Lemma SameSCAs_pop_SCA': forall (av : Type) (st : StringMap.t (Value av)) (k : StringMap.key) (ext : StringMap.t (Value av)) (v : W), k ∉ ext -> SameSCAs ext st -> SameSCAs ext ([k |> wrap v]::st).
proof: Proof. unfold SameSCAs; map_iff; intros; repeat match goal with | [ H: ?k ∉ ?m, H': StringMap.MapsTo ?k' _ ?m |- _ ] => learn (MapsTo_NotIn_inv H H') | [ H: forall _ _ , _ <-> _, H': _ |- _ ] => rewrite_in H H' | [ H: forall _ _ , _ <-> _ |- _ ] => rewrite H | _ => solve [intuition discriminate] end. eauto using StringMap.add_2. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas