2 simple JSON questions

Stream: lean4

[Julian Berman]

Do these instances belong in Lean, and/or is the recursion gymnastics I assume is necessary to prove them the reason they're not there?

instance {a₁ a₂ : Array Json} : Decidable (a₁ = a₂) := sorry
instance {o₁ o₂ : RBNode String fun x => Json} : Decidable (o₁ = o₂) := sorry
instance : DecidableEq Json := λ a b => by cases a <;> cases b <;> simp <;> infer_instance

Also, for my edification, is there a benefit to making JSON objects RBMap / RBNodes vs PersistentHashMaps?

[Arthur Paulino]

RB structures should exclude the possibility of hash collisions with certainty, that's one advantage