proposition: Lemma noret_cast_nop : forall (E : Type -> Type) (A : Type) (t : itree E A), all_infinite t -> t ≈ noret_cast t.
proof: Proof. intros. apply euttNoRet_subrel. apply noret_bind_nop. auto. Qed.
imports: Coq(Morphisms ) ITree(Axioms ITree ITreeFacts Props.Infinite ) Paco(paco)