proposition: Lemma interp_id_h {A R} (t : itree A R) : interp (id_ A) t ≳ t.
proof: Proof. revert t. ginit. pcofix CIH. intros. rewrite (itree_eta t), unfold_interp. destruct (observe t); try (gstep; constructor; auto with paco). cbn. gstep. red; cbn. constructor; red; intros. ITree.fold_subst. rewrite bind_ret_l, tau_euttge. eauto with paco. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Interp Interp.Handler Interp.TranslateFacts)