proposition: Lemma eutt_equiv {E} {R S} {RS RS'} : forall (t : itree E R) (s : itree E S), (HeterogeneousRelations.eq_rel RS RS') -> eutt RS t s <-> eutt RS' t s.
proof: Proof. intros * EQ; split; intros EUTT; eapply eqit_mon; try apply EUTT; eauto. all:apply EQ. Qed.
imports: Coq(Setoid Morphisms Relations) Paco(paco) ITree(Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.Paco2 Eq.Shallow)