proposition: Lemma classic_converge : forall (E : Type -> Type) (A : Type) (t : itree E A), (exists a, may_converge a t) \/ all_infinite t.
proof: Proof. intros. destruct (classic (exists a, may_converge a t) ); auto. right. apply not_converge_to_all_infinite. intros a Hcontra. apply H. exists a. auto. Qed.
imports: Coq(Setoid Morphisms RelationClasses) Paco(paco) ITree(Axioms Basics Core.ITreeDefinition Eq.Eqit Eq.Shallow)