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