proposition: Lemma euttNoRet_subrel : forall (E : Type -> Type) (A B : Type) (R : A -> B -> Prop) (ta : itree E A) (tb : itree E B), euttNoRet ta tb -> eutt R ta tb.
proof: Proof. intros. eapply eutt_subrel with (R1 := fun a b => False); tauto. Qed.
imports: Coq(Morphisms ) ITree(Axioms ITree ITreeFacts Props.Infinite ) Paco(paco)