∀ (motive : (x x_1 : ONote) → (x_2 : ℕ) → x.NF → x.split' = (x_1, x_2) → Prop) (x x_1 : ONote) (x_2 : ℕ) (x_3 : x.NF)
  (x_4 : x.split' = (x_1, x_2)),
  (∀ (o' : ONote) (m : ℕ) (x : ONote.NF 0) (p : ONote.split' 0 = (o', m)), motive ONote.zero o' m x p) →
    (∀ (e : ONote) (n : ℕ+) (a o' : ONote) (m : ℕ) (h : (e.oadd n a).NF) (p : (e.oadd n a).split' = (o', m)),
        motive (e.oadd n a) o' m h p) →
      motive x x_1 x_2 x_3 x_4