{motive_1 : Lean.Elab.Tactic.RCases.RCasesPatt → Sort u} →
  {motive_2 : List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u} →
    (t : Lean.Elab.Tactic.RCases.RCasesPatt) →
      ((ref : Lean.Syntax) →
          (a : Lean.Elab.Tactic.RCases.RCasesPatt) →
            motive_1 a → motive_1 (Lean.Elab.Tactic.RCases.RCasesPatt.paren ref a)) →
        ((ref : Lean.Syntax) → (a : Lean.Name) → motive_1 (Lean.Elab.Tactic.RCases.RCasesPatt.one ref a)) →
          ((ref : Lean.Syntax) → motive_1 (Lean.Elab.Tactic.RCases.RCasesPatt.clear ref)) →
            ((ref : Lean.Syntax) →
                (a : Lean.Elab.Tactic.RCases.RCasesPatt) →
                  motive_1 a → motive_1 (Lean.Elab.Tactic.RCases.RCasesPatt.explicit ref a)) →
              ((ref : Lean.Syntax) →
                  (a : Lean.Elab.Tactic.RCases.RCasesPatt) →
                    (a_1 : Lean.Term) → motive_1 a → motive_1 (Lean.Elab.Tactic.RCases.RCasesPatt.typed ref a a_1)) →
                ((ref : Lean.Syntax) →
                    (a : List Lean.Elab.Tactic.RCases.RCasesPatt) →
                      motive_2 a → motive_1 (Lean.Elab.Tactic.RCases.RCasesPatt.tuple ref a)) →
                  ((ref : Lean.Syntax) →
                      (a : List Lean.Elab.Tactic.RCases.RCasesPatt) →
                        motive_2 a → motive_1 (Lean.Elab.Tactic.RCases.RCasesPatt.alts ref a)) →
                    motive_2 [] →
                      ((head : Lean.Elab.Tactic.RCases.RCasesPatt) →
                          (tail : List Lean.Elab.Tactic.RCases.RCasesPatt) →
                            motive_1 head → motive_2 tail → motive_2 (head :: tail)) →
                        motive_1 t