Post #4299217

The latest Lean soundness hole (https://github.com/leanprover/lean4/issues/14576), which also affects alternative implementations of the kernel, is proof that God only ever intended for us to use W-types, and certainly not nested inductives.