refactor: remove asymmetry between singleton and cons in ValidJsonArray

Problem

ValidJsonArray has separate singleton and cons constructors, creating asymmetry. A uniform nil / cons inductive pattern would be simpler and more consistent with standard list-shaped inductives in Lean/Mathlib.

Expected fix

Refactor ValidJsonArray to use a uniform nil/cons structure. Verify that all downstream proofs (Proofs.lean) still hold with the refactored definition.

References

• Suggested by AI code review on PR #8

ValidJsonArray の定義を見つけ、Proofs.lean を読んで、下流のすべての使用箇所と証明義務を特定します。構造体を統一された nil/cons 形式にリファクタリングし、既存の証明が引き続きコンパイルされ、成立することを確認します。