(motive : Array Unit × Lean.Elab.Term.ToDepElimPattern.TopSort.State → Sort u_1) →
  (__discr : Array Unit × Lean.Elab.Term.ToDepElimPattern.TopSort.State) →
    ((fst : Array Unit) → (s : Lean.Elab.Term.ToDepElimPattern.TopSort.State) → motive (fst, s)) → motive __discr