{α : Type} →
  (left right : Subarray α) →
    (motive : Option (ℕ × α × Fin left.size × Fin right.size) → Sort u_1) →
      (best : Option (ℕ × α × Fin left.size × Fin right.size)) →
        ((fst : ℕ) → (v : α) → (li : Fin left.size) → (ri : Fin right.size) → motive (some (fst, v, li, ri))) →
          ((x : Option (ℕ × α × Fin left.size × Fin right.size)) → motive x) → motive best