proposition: Lemma eutt_eq_itree {E X} (R : X -> X -> Prop) : forall (t : itree E X), eutt R t t -> eq_itree R t t.
proof: Proof. enough (forall (t u : itree E X), eutt R t u -> eq_itree eq t u -> eq_itree R t u). { intros; apply H; [ auto | apply Reflexive_eqit_eq ]. } pcofix CIH. intros t u H EQ. pfold. red. rewrite (itree_eta t), (itree_eta u) in H. punfold EQ. destruct EQ; try discriminate; constructor. - rewrite <- eutt_Ret in H. auto. - pclearbot. right; apply CIH; [ | apply REL ]. revert H; apply eqit_Tau. - pclearbot. right; apply CIH; [ | apply REL ]. eapply eqit_inv_Vis with (1 := H). Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)