proposition: Lemma WeakEq_add_MapsTo : forall {av} k v m1 m2, StringMap.MapsTo k v m1 -> WeakEq (StringMap.add k v m1) m2 -> @WeakEq av m1 m2.
proof: Proof. intros; rewrite add_redundant_cancel; eassumption. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas