proposition: Lemma interp_recursive_call {E A B} (f : A -> itree (callE A B +' E) B) (x:A) : interp (recursive f) (call x) ≈ rec f x.
proof: Proof. unfold recursive. unfold call. rewrite interp_trigger. cbn. 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)