proposition: Lemma all_infinite_bind : forall (E : Type -> Type) (R U: Type) (t : itree E R) (f : R -> itree E U), all_infinite t -> all_infinite (bind t f).
proof: Proof. intros. apply noret_bind_nop with (B := U) (f := f) in H. apply euttNoRet_sym in H. apply euttNoRet_all_infinite in H. auto. Qed.
imports: Coq(Morphisms ) ITree(Axioms ITree ITreeFacts Props.Infinite ) Paco(paco)