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