∀ (motive : Lean.Doc.ArgSpec✝ → Sort u_1) (a : Lean.Name) (a_1 a_2 : Lean.Expr)
  (h_1 : (a : Lean.Name) → (a_3 : Lean.Expr) → motive (Lean.Doc.ArgSpec.positional✝ a a_3))
  (h_2 : (a : Lean.Name) → (a_3 a_4 : Lean.Expr) → motive (Lean.Doc.ArgSpec.named✝ a a_3 a_4))
  (h_3 : (a : Lean.Name) → (a_3 : Lean.Expr) → motive (Lean.Doc.ArgSpec.many✝ a a_3))
  (h_4 : (a : Lean.Name) → (a_3 : Bool) → motive (Lean.Doc.ArgSpec.flag✝ a a_3)),
  (match Lean.Doc.ArgSpec.named✝¹ a a_1 a_2 with
    | Lean.Doc.ArgSpec.positional✝¹ a a_3 => h_1 a a_3
    | Lean.Doc.ArgSpec.named✝² a a_3 a_4 => h_2 a a_3 a_4
    | Lean.Doc.ArgSpec.many✝¹ a a_3 => h_3 a a_3
    | Lean.Doc.ArgSpec.flag✝¹ a a_3 => h_4 a a_3) =
    h_2 a a_1 a_2