proposition: Lemma has_post_weaken : forall {E X} (t : itree E X) P Q, t ⤳ P -> P <1= Q -> t ⤳ Q.
proof: Proof. intros * HP INCL. eapply eqit_mon; eauto. intros; apply INCL; auto. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)