proposition: Lemma rec_as_interp {E A B} (f : A -> itree (callE A B +' E) B) (x : A) : rec f x ≈ interp (recursive f) (f x).
proof: Proof. unfold rec. rewrite mrec_as_interp. apply eq_sub_eutt. eapply eq_itree_interp. - red. unfold case_; intros ? [[] | ]; reflexivity. - reflexivity. Qed.
imports: Paco.paco Coq(Program.Tactics Setoid Morphisms) ITree(Basics.Utils Basics.Category Basics.Basics Basics.Function Core.ITreeDefinition Core.KTree Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Handler Interp.Interp Interp.InterpFacts Interp.Recursion)