proposition: Lemma WeakEq_pop_SCA_left : forall {av} k (v: W) (m1 m2: StringMap.t (Value av)), k ∉ m1 -> WeakEq (StringMap.add k (wrap v) m1) m2 -> WeakEq m1 m2.
proof: Proof. unfold WeakEq; intuition eauto using SameADTs_pop_SCA_left, SameSCAs_pop_SCA_left. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas