(motive : List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u_1) →
  (x : List Lean.Elab.Tactic.RCases.RCasesPatt) →
    (Unit → motive []) →
      ((ref : Lean.Syntax) → motive [Lean.Elab.Tactic.RCases.RCasesPatt.tuple ref []]) →
        ((ref : Lean.Syntax) →
            (ps : List Lean.Elab.Tactic.RCases.RCasesPatt) → motive [Lean.Elab.Tactic.RCases.RCasesPatt.tuple ref ps]) →
          ((p : Lean.Elab.Tactic.RCases.RCasesPatt) →
              (ps : List Lean.Elab.Tactic.RCases.RCasesPatt) → motive (p :: ps)) →
            motive x