proposition: Lemma subevent_left {E F R} (e: E R): @subevent E (E +' F) (ReSum_inl _ _ _ _ _) R e = inl1 e.
proof: Proof. reflexivity. Qed.
imports: ITree(Basics.Basics Basics.CategoryOps Core.ITreeDefinition Indexed.Sum Indexed.Function)