proposition: Lemma noret_bind_nop : forall (E : Type -> Type) (A B : Type) (t : itree E A) (f : A -> itree E B), all_infinite t -> euttNoRet t (t >>= f).
proof: Proof. intros. einit. generalize dependent t. ecofix CIH. intros t Hdivt. pinversion Hdivt. - specialize (itree_eta t) as Ht. rewrite <- H in Ht. cbn. rewrite Ht. assert (ITree.bind (Tau t0) f ≅ Tau (ITree.bind t0 f)); try apply bind_tau. setoid_rewrite H1. etau. - specialize (itree_eta t) as Ht. rewrite <- H in Ht. cbn. rewrite Ht. rewrite bind_vis. evis. Qed.
imports: Coq(Morphisms ) ITree(Axioms ITree ITreeFacts Props.Infinite ) Paco(paco)