{α : Type} →
  (motive : MProd ℕ (MProd ℕ (Array (Lean.Diff.Action × α))) → Sort u_1) →
    (r : MProd ℕ (MProd ℕ (Array (Lean.Diff.Action × α)))) →
      ((i j : ℕ) → (out : Array (Lean.Diff.Action × α)) → motive ⟨i, j, out⟩) → motive r