proposition: Lemma WeakEq_remove_notIn: forall av (k : StringMap.key) (st1 st2 : State av), k ∉ st1 -> WeakEq st1 st2 -> WeakEq st1 (StringMap.remove k st2).
proof: Proof. intros. rewrite <- (remove_notIn_Equal (k := k) (m := st1)) by assumption. eauto using WeakEq_remove. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas