proposition: Lemma interp_map_id d {E X} (t : itree (mapE K d +' E) X) : map_default_eq eq d (interp_map t) (interp_map t).
proof: Proof. unfold map_default_eq, interp_map; intros. revert t s1 s2 H. ginit. pcofix CH. intros. repeat rewrite unfold_interp_state. unfold _interp_state. destruct (observe t). - gstep. constructor. constructor; auto. - gstep. constructor. gbase. apply CH. assumption. - guclo eqit_clo_bind. econstructor. unfold pure_state. destruct e. + cbn. eapply eqit_mon; [ exact (fun x => x) .. | | apply handle_map_eq; assumption ]. auto. auto. intros. apply PR. + cbn. apply eqit_Vis. intros. apply eqit_Ret. constructor; auto. + intros. destruct u1. destruct u2. cbn. destruct H as [H1 H2]; cbn in H1, H2; subst. gstep; constructor. gbase. apply CH. assumption. Qed.
imports: Coq(Morphisms) ExtLib(Core.RelDec) Paco(paco) ITree(Basics.HeterogeneousRelations ITree ITreeFacts Eq.Paco2 Events.State Events.StateFacts Events.MapDefault)