proposition: Lemma has_post_bind_weak : forall {E X Y} (t : itree E X) (k : X -> itree E Y) Q, (forall x, k x ⤳ Q) -> ITree.bind t k ⤳ Q.
proof: Proof. intros * POST. apply eutt_eq_bind; intros ?; apply POST. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)