proposition: Lemma map_tau {E A B} (f : A -> B) (t : itree E A) : @ITree.map E _ _ f (Tau t) ≅ Tau (ITree.map f t).
proof: Proof. intros. unfold ITree.map. rewrite bind_tau; 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)