proposition: Lemma SameValues_remove_SCA: forall (av : Type) {A} (Wrapper: FacadeWrapper (Value av) A), (forall a, is_adt (wrap a) = false) -> forall (tenv' : Telescope av) (ext : StringMap.t (Value av)) (k : StringMap.key) (final_state : State av) (x : A), StringMap.MapsTo k (wrap x) final_state -> StringMap.remove (elt:=Value av) k final_state ≲ tenv' ∪ ext -> final_state ≲ tenv' ∪ ext.
proof: Proof. induction tenv'; simpl; intros. - rewrite (add_redundant_cancel H0). rewrite <- add_remove_cancel; try reflexivity. pose proof (H x) as p; destruct (wrap x); simpl in p; try congruence; clear p. apply WeakEq_pop_SCA. apply StringMap.remove_1; reflexivity. assumption. - destruct key; repeat cleanup. + eauto. + SameValues_Fiat_t. StringMap_t. rewrite remove_mapsto_iff in *. cleanup. StringMap_t. eexists; repeat cleanup; eauto. eapply H0. rewrite remove_mapsto_iff in *; eauto. rewrite remove_remove_comm; eauto. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas