proposition: Lemma eutt_subrel : forall (E : Type -> Type) (A B : Type) (R1 R2 : A -> B -> Prop) (ta : itree E A) (tb : itree E B), (forall a b, R1 a b -> R2 a b) -> eutt R1 ta tb -> eutt R2 ta tb.
proof: Proof. intros. eapply eqit_mon; eauto. Qed.
imports: Paco(paco) ITree(Core.ITreeDefinition Eq.Eqit)