feat: implement To/FromJSON Empty

[TomasPuverle]

Resolve cases when the To/FromJSON type classes are used with Empty, e.g. in the following motivating example.

import Lean

structure Foo (α : Type) where
  y : Option α
deriving Lean.ToJson

#eval Lean.toJson (⟨none⟩ : Foo Empty) -- fails

This is a follow-up to this PR #5415, as suggested by @eric-wieser. It expands on the original suggestion by also handling FromJSON.

[TomasPuverle]

CC: @kmill in case interested/relevant.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 738435b90aaa251a731cc463d6e49560f2037df9 --onto a6830f90ab365e14ccb7ca31201de37f8c1e978c. (2024-09-23 03:47:18)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 738435b90aaa251a731cc463d6e49560f2037df9 --onto e551a366a0bbb27d5f853cc8e87cbd381a76ffc0. (2024-09-23 20:32:15)

[TomasPuverle]

🎉