proposition: Lemma translate_trigger {E F G} `{E -< F} : forall X (e: E X) (h: F ~> G), translate h (trigger e) ≈ trigger (h _ (subevent X e)).
proof: Proof. intros; unfold trigger; rewrite translate_vis; setoid_rewrite translate_ret; reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(Basics.Basics Basics.Category Core.ITreeDefinition Core.Subevent Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Interp)