proposition: Lemma eqitree_inv_Tau_r {E R} (t t' : itree E R) : t ≅ Tau t' -> exists t0, observe t = TauF t0 /\ t0 ≅ t'.
proof: Proof. intros; punfold H; inv H; try inv CHECK; pclearbot; eauto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)