(motive : MProd (Array Lean.Name) (MProd ℕ (Array Lean.Expr)) → Sort u_1) →
  (r : MProd (Array Lean.Name) (MProd ℕ (Array Lean.Expr))) →
    ((eqnNames : Array Lean.Name) → (idx : ℕ) → (notAlts : Array Lean.Expr) → motive ⟨eqnNames, idx, notAlts⟩) →
      motive r