proposition: Theorem sutt_eutt {E R1 R2} (RR : R1 -> R2 -> Prop) : forall (t1 : itree E R1) (t2 : itree E R2), sutt RR t1 t2 -> sutt (flip RR) t2 t1 -> eutt RR t1 t2.
proof: Proof. pcofix CIH. intros. punfold H0. punfold H. pstep. red. induction H0; intros; subst; auto with itree. - constructor. intro. right. eapply suttF_inv_vis in H. pclearbot. eauto with paco itree. - constructor; eauto. eapply IHsuttF; auto. eapply suttF_inv_tau_left; auto. - inv H; pclearbot. + clear t1 t2. genobs t0 ot0. hinduction EQTAUS0 before CIH; intros; subst; pclearbot. * constructor; eauto. simpobs. constructor. eauto. * constructor; eauto. simpobs. constructor. intros. right. apply CIH; auto with itree. eapply sutt_inv_vis in EQTAUS; eauto with itree. * constructor; eauto. simpobs. eapply IHEQTAUS0; eauto. rewrite (itree_eta' ot1). apply sutt_inv_tau_left; auto. * constructor. right. apply CIH; auto. apply sutt_elim_tau_right; auto. + constructor. right. apply CIH; apply sutt_elim_tau_right; auto. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Axioms Basics.Utils Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.Shallow Eq.Paco2)