proposition: Lemma any_infiniteF__mono {E X} : monotone1 (@any_infinite_ E X).
proof: Proof. do 2 red. intros. eapply any_infiniteF_mono; eauto. Qed.
imports: Coq(Setoid Morphisms RelationClasses) Paco(paco) ITree(Axioms Basics Core.ITreeDefinition Eq.Eqit Eq.Shallow)