proposition: Lemma all_infinite_not_converge : forall (E : Type -> Type) (R : Type) (t : itree E R) (r : R), may_converge r t -> ~ all_infinite t.
proof: Proof. intros E R t r Hc Hd. induction Hc. - rewrite H in Hd. pinversion Hd. - apply IHHc. rewrite H in Hd. pinversion Hd. ddestruction. subst. apply H1. Qed.
imports: Coq(Setoid Morphisms RelationClasses) Paco(paco) ITree(Axioms Basics Core.ITreeDefinition Eq.Eqit Eq.Shallow)