(motive : Option (Array (Lean.TSyntaxArray `block)) → Sort u_1) →
  (x : Option (Array (Lean.TSyntaxArray `block))) →
    ((itemss : Array (Lean.TSyntaxArray `block)) → motive (some itemss)) → (Unit → motive none) → motive x