{ks : Lean.SyntaxNodeKinds} →
  {sep : String} →
    {motive : Lean.Syntax.TSepArray ks sep → Sort u} →
      ((elemsAndSeps : Array Lean.Syntax) → motive { elemsAndSeps := elemsAndSeps }) →
        (t : Lean.Syntax.TSepArray ks sep) → motive t