proposition: Lemma eqitree_Tau {E R} (t1 t2 : itree E R): Tau t1 ≅ Tau t2 <-> t1 ≅ t2.
proof: Proof. apply eqit_Tau. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)