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