proposition: Lemma tau_eutt {E R} (t: itree E R) : Tau t ≈ t.
proof: Proof. apply euttge_sub_eutt, tau_euttge. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)