∀ (motive : ONote × ℕ → Sort u_1) (a0 : ONote) (a : ℕ+) (a_1 : ONote) (m : ℕ) (h_1 : Unit → motive (ONote.zero, 0))
  (h_2 : Unit → motive (ONote.zero, 1)) (h_3 : (m : ℕ) → motive (ONote.zero, m.succ))
  (h_4 : (a a0 : ONote) → (a_2 : ℕ+) → (a_3 : ONote) → a = a0.oadd a_2 a_3 → (m : ℕ) → motive (a0.oadd a_2 a_3, m)),
  (match (a0.oadd a a_1, m) with
    | (ONote.zero, 0) => h_1 ()
    | (ONote.zero, 1) => h_2 ()
    | (ONote.zero, m.succ) => h_3 m
    | (a@h:(a0.oadd a_2 a_3), m) => h_4 a a0 a_2 a_3 h m) =
    h_4 (a0.oadd a a_1) a0 a a_1 ⋯ m