(motive : Option (Array (Lean.TSyntax `ident)) → Sort u_1) →
  (x : Option (Array (Lean.TSyntax `ident))) →
    ((ns : Array (Lean.TSyntax `ident)) → motive (some ns)) → (Unit → motive none) → motive x