proposition: Lemma map_ret {E A B} (f : A -> B) (a : A) : @ITree.map E _ _ f (Ret a) ≅ Ret (f a).
proof: Proof. intros. unfold ITree.map. 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)