proposition: Lemma has_post_conj : forall {E X} (t : itree E X) P Q, t ⤳ P -> t ⤳ Q -> t ⤳ (P /1\ Q).
proof: Proof. intros * HP HQ. pose proof eutt_conj _ _ HP HQ. auto. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)