proposition: Lemma tau_eutt_RR_r : forall E R (RR : relation R) (HRR: Reflexive RR) (HRT: Transitive RR) (t s : itree E R), eutt RR t (Tau s) <-> eutt RR t s.
proof: Proof. intros. split; intros H. - eapply transitivity. apply H. red. apply eqit_Tau_l. reflexivity. - red. red. pstep. econstructor. auto. punfold H. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)