{motive_1 : Lean.Parser.Tactic.MRefinePat → Sort u} →
  {motive_2 : List Lean.Parser.Tactic.MRefinePat → Sort u} →
    ((name : Lean.TSyntax `Lean.binderIdent) → motive_1 (Lean.Parser.Tactic.MRefinePat.one name)) →
      ((args : List Lean.Parser.Tactic.MRefinePat) →
          motive_2 args → motive_1 (Lean.Parser.Tactic.MRefinePat.tuple args)) →
        ((h : Lean.TSyntax `term) → motive_1 (Lean.Parser.Tactic.MRefinePat.pure h)) →
          ((h : Lean.TSyntax `Lean.binderIdent) → motive_1 (Lean.Parser.Tactic.MRefinePat.stateful h)) →
            ((name : Lean.TSyntax `Lean.binderIdent) → motive_1 (Lean.Parser.Tactic.MRefinePat.hole name)) →
              motive_2 [] →
                ((head : Lean.Parser.Tactic.MRefinePat) →
                    (tail : List Lean.Parser.Tactic.MRefinePat) →
                      motive_1 head → motive_2 tail → motive_2 (head :: tail)) →
                  (t : List Lean.Parser.Tactic.MRefinePat) → motive_2 t