proposition: Lemma all_infiniteF_mono {E A} (sim sim' : itree E A -> Prop) t (IN : all_infiniteF sim t) (LE : sim <1= sim') : all_infiniteF sim' t.
proof: Proof. induction IN; eauto with itree. Qed.
imports: Coq(Setoid Morphisms RelationClasses) Paco(paco) ITree(Axioms Basics Core.ITreeDefinition Eq.Eqit Eq.Shallow)