proposition: Lemma subevent_subevent : forall {E F G :Type -> Type} (SEF: E -< F) (SFG: F -< G) T (e : E T), @subevent F G SFG T (@subevent E F SEF T e) = @subevent E G (fun x f => SFG _ (SEF _ f)) T e.
proof: Proof. reflexivity. Qed.
imports: ITree(Basics.Basics Basics.CategoryOps Core.ITreeDefinition Indexed.Sum Indexed.Function)