∀ (motive : Lean.Syntax → Sort u_1) (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax)
  (h_1 :
    (s : Lean.Syntax) →
      (info : Lean.SourceInfo) →
        (kind : Lean.SyntaxNodeKind) →
          (args : Array Lean.Syntax) → s = Lean.Syntax.node info kind args → motive (Lean.Syntax.node info kind args))
  (h_2 : (x : Lean.Syntax) → motive x),
  (match Lean.Syntax.node info kind args with
    | s@h:(Lean.Syntax.node info kind args) => h_1 s info kind args h
    | x => h_2 x) =
    h_1 (Lean.Syntax.node info kind args) info kind args ⋯