proposition: Lemma has_post_translate : forall {E F X} (t : itree E X) Q (h : E ~> F), t ⤳ Q -> translate h t ⤳ Q.
proof: Proof. unfold has_post; intros * POST. apply eutt_translate_gen; auto. Qed.
imports: Paco(paco) Coq(Morphisms) ITree(Basics.Utils ITree Eq.Eqit Basics.HeterogeneousRelations Interp.TranslateFacts)