(motive : List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u_1) →
  (ps : List Lean.Elab.Tactic.RCases.RCasesPatt) →
    (Unit → motive []) →
      ((p : Lean.Elab.Tactic.RCases.RCasesPatt) → motive [p]) →
        ((ps : List Lean.Elab.Tactic.RCases.RCasesPatt) →
            (ps = [] → False) → (∀ (p : Lean.Elab.Tactic.RCases.RCasesPatt), ps = [p] → False) → motive ps) →
          motive ps