(motive : Lean.Meta.Match.Pattern → Sort u_1) →
  (x : Lean.Meta.Match.Pattern) →
    ((e : Lean.Expr) → motive (Lean.Meta.Match.Pattern.inaccessible e)) →
      ((e : Lean.Expr) → motive (Lean.Meta.Match.Pattern.val e)) →
        ((n : Lean.Name) →
            (us : List Lean.Level) →
              (ps : List Lean.Expr) →
                (fields : List Lean.Meta.Match.Pattern) → motive (Lean.Meta.Match.Pattern.ctor n us ps fields)) →
          ((x : Lean.FVarId) →
              (p : Lean.Meta.Match.Pattern) → (h : Lean.FVarId) → motive (Lean.Meta.Match.Pattern.as x p h)) →
            ((t : Lean.Expr) → (xs : List Lean.Meta.Match.Pattern) → motive (Lean.Meta.Match.Pattern.arrayLit t xs)) →
              ((p : Lean.Meta.Match.Pattern) → motive p) → motive x