proposition: Lemma map_map {E R S T}: forall (f : R -> S) (g : S -> T) (t : itree E R), ITree.map g (ITree.map f t) ≅ ITree.map (fun x => g (f x)) t.
proof: Proof. unfold ITree.map. intros. rewrite bind_bind. setoid_rewrite bind_ret_l. reflexivity. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)