proposition: Lemma interp_state_trigger_eqit {E F : Type -> Type} {R S : Type} (e : E R) (f : E ~> Monads.stateT S (itree F)) (s : S) : (interp_state f (ITree.trigger e) s) ≅ (f _ e s >>= fun x => Tau (Ret x)).
proof: Proof. unfold ITree.trigger. rewrite interp_state_vis. eapply eqit_bind; try reflexivity. intros []. rewrite interp_state_ret. reflexivity. Qed.
imports: Coq(Program.Tactics Morphisms) Paco(paco) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.HeterogeneousRelations Basics.Monad Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Interp.Interp Interp.InterpFacts Interp.RecursionFacts Events.State)