proposition: Lemma resum_to_subevent : forall (E F : Type -> Type) H T e, @resum _ IFun E F H T e = subevent _ e.
proof: Proof. intros; reflexivity. Qed.
imports: ITree(Basics.Basics Basics.CategoryOps Core.ITreeDefinition Indexed.Sum Indexed.Function)