proposition: Lemma SameADTs_pop_SCA_util: forall (av : Type) (st : StringMap.t (Value av)) (k : StringMap.key) (v : W), not_mapsto_adt k st = true -> SameADTs st ([k |> wrap v]::st).
proof: Proof. intros ** k' v; destruct (StringMap.E.eq_dec k k'); subst; split; intros; repeat match goal with | _ => progress map_iff | _ => progress not_mapsto_adt_t | [ H: not_mapsto_adt ?k ?st = true, H': StringMap.MapsTo ?k (ADT ?v) ?st |- _ ] => destruct (not_mapsto_adt_not_MapsTo_ADT H H') | [ H: context[@StringMap.MapsTo] |- _ ] => progress map_iff_in H end. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas