proposition: Lemma rutt_flip {E1 E2 R1 R2 REv RAns RR} (t1: itree E1 R1) (t2: itree E2 R2): rutt REv RAns RR t1 t2 <-> rutt (flip_REv REv) (flip_RAns RAns) (flip RR) t2 t1.
proof: Proof. split; revert t1 t2; pcofix CIH; intros t1 t2 Hrutt; punfold Hrutt; red in Hrutt; pstep; red. - induction Hrutt; try now constructor. * apply EqTau. right. apply CIH. now pclearbot. * apply EqVis. auto. intros b a HAns. cbn in HAns. right. specialize (H0 a b HAns). apply CIH. now pclearbot. - induction Hrutt; try now constructor. * apply EqTau. right. apply CIH. now pclearbot. * apply EqVis. auto. intros b a HAns. cbn in HAns. right. specialize (H0 a b HAns). apply CIH. now pclearbot. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(ITree ITreeFacts Core.Subevent Basics.HeterogeneousRelations Eq.Rutt Props.Leaf)