proposition: Lemma noret_cast_cast E (A B : Type) (t1 t2 : itree E A) (R : A -> A -> Prop) (R' : B -> B -> Prop) : all_infinite t1 -> eutt R t1 t2 -> eutt R' (noret_cast t1) (noret_cast t2).
proof: Proof. intros. apply euttNoRet_subrel. apply all_infinite_euttNoRet in H0; auto. infer_noret H0. apply euttNoRet_trans with (t2 := t2); try apply noret_bind_nop; auto. apply euttNoRet_trans with (t2 := t1); auto. apply euttNoRet_sym. apply noret_bind_nop. auto. Qed.
imports: Coq(Morphisms ) ITree(Axioms ITree ITreeFacts Props.Infinite ) Paco(paco)