proposition: Lemma euttNoRet_trans : forall (E : Type -> Type) (A B C : Type) (t1 : itree E A) (t2 : itree E B) (t3 : itree E C), euttNoRet t1 t2 -> euttNoRet t2 t3 -> euttNoRet t1 t3.
proof: Proof. intros. unfold euttNoRet in *. apply eutt_subrel with (R1 := @rcompose A B C (fun a b => False) (fun b c => False) ). - intros. inversion H1; contradiction. - eapply eqit_trans; eauto. Qed.
imports: Coq(Morphisms ) ITree(Axioms ITree ITreeFacts Props.Infinite ) Paco(paco)