proposition: Lemma any_infiniteF_mono {E X} sim sim' x0 (IN: any_infiniteF sim x0) (LE: sim <1= sim'): @any_infiniteF E X sim' x0.
proof: Proof. intros. induction IN; eauto with itree. Qed.
imports: Coq(Setoid Morphisms RelationClasses) Paco(paco) ITree(Axioms Basics Core.ITreeDefinition Eq.Eqit Eq.Shallow)