proposition: Theorem spin_infinite {E A} : @any_infinite E A ITree.spin.
proof: Proof. unfold any_infinite, ITree.spin. pcofix H. pfold. constructor. right. apply H. Qed.
imports: Coq(Setoid Morphisms RelationClasses) Paco(paco) ITree(Axioms Basics Core.ITreeDefinition Eq.Eqit Eq.Shallow)