proposition: Lemma eq_map_remove: forall (d : V) (s1 s2 : map) (k : K), (@eq_map _ _ _ _ d) s1 s2 -> (@eq_map _ _ _ _ d) (remove k s1) (remove k s2).
proof: Proof. intros d s1 s2 k H. unfold eq_map in *; intros k'. unfold lookup_default. destruct (rel_dec_p k k'). - subst; rewrite 2 lookup_remove_eq; auto. - rewrite 2 lookup_remove_neq; auto. apply H. Qed.
imports: Coq(Morphisms) ExtLib(Core.RelDec) Paco(paco) ITree(Basics.HeterogeneousRelations ITree ITreeFacts Eq.Paco2 Events.State Events.StateFacts Events.MapDefault)