proposition: Lemma euttNoRet_spin : forall (E : Type -> Type) (A B : Type), @euttNoRet E A B ITree.spin ITree.spin.
proof: Proof. intros. pcofix CIH. pfold. red. cbn. constructor. right. eauto. Qed.
imports: Coq(Morphisms ) ITree(Axioms ITree ITreeFacts Props.Infinite ) Paco(paco)