proposition: Lemma eutt_translate_gen : forall {E F X Y} (f : E ~> F) (RR : X -> Y -> Prop) (t : itree E X) (s : itree E Y), eutt RR t s -> eutt RR (translate f t) (translate f s).
proof: Proof. intros *. revert t s. einit. ecofix CIH. intros * EUTT. rewrite !unfold_translate. punfold EUTT. red in EUTT. induction EUTT; intros; subst; simpl; pclearbot. - estep. - estep. - estep; intros ?; ebase. - rewrite tau_euttge, unfold_translate. eauto with itree. - rewrite tau_euttge, unfold_translate. eauto with 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)