proposition: Lemma has_post_bind : forall {E X Y} (t : itree E X) (k : X -> itree E Y) S Q, t ⤳ S -> (forall x, S x -> k x ⤳ Q) -> ITree.bind t k ⤳ Q.
proof: Proof. intros * POST1 POST2. apply eutt_clo_bind with (UU := fun x y => x = y /\ S x) ; [apply has_post_post_strong; exact POST1 |]. intros ? ? [<- ?]; eapply POST2; eauto. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)