proposition: Lemma not_converge_to_all_infinite : forall (E : Type -> Type) (A : Type) (t : itree E A), (forall a, ~ may_converge a t) -> all_infinite t.
proof: Proof. intros E A. pcofix CIH. intros t Hcon. pfold. red. destruct (observe t) eqn : Heq; specialize (itree_eta t) as Ht; rewrite Heq in Ht. - exfalso. apply (Hcon r0). rewrite Ht. constructor. reflexivity. - constructor. right. apply CIH. setoid_rewrite Ht in Hcon. setoid_rewrite tau_eutt in Hcon. auto. - constructor. right. apply CIH. intros a Hcontra. setoid_rewrite Ht in Hcon. apply (Hcon a). eapply conv_vis; try reflexivity; eauto. Qed.
imports: Coq(Setoid Morphisms RelationClasses) Paco(paco) ITree(Axioms Basics Core.ITreeDefinition Eq.Eqit Eq.Shallow)