proposition: Lemma handle_map_eq : forall d E X (s1 s2 : map) (m : mapE K d X), (@eq_map _ _ _ _ d) s1 s2 -> eutt (prod_rel (@eq_map _ _ _ _ d) eq) (handle_map m s1) ((handle_map m s2) : itree E (map * X)).
proof: Proof. intros. destruct m; cbn; red; apply eqit_Ret; constructor; cbn; auto. - apply eq_map_add. assumption. - apply eq_map_remove. assumption. Qed.
imports: Coq(Morphisms) ExtLib(Core.RelDec) Paco(paco) ITree(Basics.HeterogeneousRelations ITree ITreeFacts Eq.Paco2 Events.State Events.StateFacts Events.MapDefault)