∀ (motive : Std.HashSet Lean.Syntax.Range → Lean.Syntax → Sort u_1) (curr : Std.HashSet Lean.Syntax.Range)
  (x : Lean.Syntax)
  (h_1 :
    (curr : Std.HashSet Lean.Syntax.Range) →
      (s : Lean.Syntax) →
        (info : Lean.SourceInfo) →
          (kind : Lean.SyntaxNodeKind) →
            (args : Array Lean.Syntax) →
              s = Lean.Syntax.node info kind args → motive curr (Lean.Syntax.node info kind args))
  (h_2 :
    (curr : Std.HashSet Lean.Syntax.Range) → (info : Lean.SourceInfo) → motive curr (Lean.Syntax.atom info "where"))
  (h_3 : (curr : Std.HashSet Lean.Syntax.Range) → (x : Lean.Syntax) → motive curr x),
  (∀ (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax),
      x = Lean.Syntax.node info kind args → False) →
    (∀ (info : Lean.SourceInfo), x = Lean.Syntax.atom info "where" → False) →
      (match curr, x with
        | curr, s@h:(Lean.Syntax.node info kind args) => h_1 curr s info kind args h
        | curr, Lean.Syntax.atom info "where" => h_2 curr info
        | curr, x => h_3 curr x) =
        h_3 curr x