proposition: Lemma unfold_translate_ : forall (t : itree E R), observing eq (translate h t) (translateF h (fun t => translate h t) (observe t)).
proof: Proof. intros t. econstructor. 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)