proposition: Lemma euttNoRet_sym : forall (E : Type -> Type) (A B : Type) (t1 : itree E A) (t2 : itree E B), euttNoRet t1 t2 -> euttNoRet t2 t1.
proof: Proof. intros E A B. pcofix CIH. intros. pfold. red. punfold H0. unfold_eqit. dependent induction H0; try contradiction; pclearbot. - rewrite <- x0. rewrite <- x. constructor. right. auto. - rewrite <- x0. rewrite <- x. constructor. intros. unfold id. right. apply CIH. apply REL. - rewrite <- x. constructor; auto. - rewrite <- x. constructor; auto. Qed.
imports: Coq(Morphisms ) ITree(Axioms ITree ITreeFacts Props.Infinite ) Paco(paco)