proposition: Lemma has_post_to_eq_itree : forall {E X} (t : itree E X) (Q : X -> Prop), has_post t Q -> eq_itree (fun x y => x = y /\ Q x) t t.
proof: Proof. intros * H; apply has_post_strong_to_eq_itree, has_post_post_strong, H. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)