proposition: Lemma has_post_True : forall {E X} (t : itree E X), t ⤳ fun _ => True.
proof: Proof. intros *. eapply eqit_mon; eauto. reflexivity. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)