proposition: Lemma interp_recursive_call : forall {E A B} (f : A -> itree (callE A B +' E) B) (x : A), interp (recursive f) (call x) ≈ rec f x.
proof: Proof. intros. rewrite ITree.Interp.RecursionFacts.interp_recursive_call. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree(Eq.Shallow) ITree.Core.ITreeDefinition ITree.Basics.Basics ITree.Indexed.Sum ITree.Interp.Interp ITree.Interp.Recursion ITree(Eq.Eqit Eq.UpToTaus Interp.InterpFacts Interp.RecursionFacts)