proposition: Lemma translate_bind : forall {E F R S} (h : E ~> F) (t : itree E S) (k : S -> itree E R), translate h (x <- t ;; k x) ≅ (x <- (translate h t) ;; translate h (k x)).
proof: Proof. intros E F R S h t k. revert S t k. ginit. pcofix CIH. intros s t k. match goal with | [ |- _ ?t1 ?t2 ] => rewrite (itree_eta_ t1), (itree_eta_ t2) end; cbn. unfold observe; cbn. destruct (observe t); cbn. - apply reflexivity. - gstep. constructor. eauto with paco. - gstep. constructor. eauto with paco itree. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(Basics.Basics Basics.Category Core.ITreeDefinition Core.Subevent Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Interp)