proposition: Lemma eutt_flip : forall (E : Type -> Type) (A B : Type) (R : A -> B -> Prop) (ta : itree E A) (tb : itree E B), eutt R ta tb -> eutt (flip R) tb ta.
proof: Proof. intros. apply eqit_flip. eapply eutt_subrel with (R1 := R); eauto. Qed.
imports: Paco(paco) ITree(Core.ITreeDefinition Eq.Eqit)