proposition: Lemma subevent_subevent' : forall {E F} `{E -< F} {X} (e : E X), @subevent F F _ X (@subevent E F _ X e) = subevent X e.
proof: Proof. reflexivity. Qed.
imports: ITree(Basics.Basics Basics.CategoryOps Core.ITreeDefinition Indexed.Sum Indexed.Function)