proposition: Lemma has_post_disj_l : forall {E X} (t : itree E X) P Q, t ⤳ P -> t ⤳ (P \1/ Q).
proof: Proof. intros * HP. epose proof eutt_disj_l _ _ HP as H. apply H. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)