proposition: Lemma translate_vis : forall X (e:E X) (k : X -> itree E R), translate h (Vis e k) ≅ Vis (h _ e) (fun x => translate h (k x)).
proof: Proof. intros X e k. rewrite itree_eta, unfold_translate. cbn. reflexivity. 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)