proposition: Lemma has_post_post_strong : forall {E X} (t : itree E X) Q, has_post t Q <-> has_post_strong t Q.
proof: Proof. intros; split; intros HP. - apply eutt_conj; [reflexivity | auto]. - eapply eqit_mon; eauto. intros * H; apply H. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)