[whateveracct]

It depends? But it's nice to have the option.

DTs doesn't mean everything is proven to the max.

Haskell already has a proven `NonEmpty` list without DTs - you can prove that with a product type alone :)

And that proof is useful because it allows you to have better proofs down the line. For instance, the min or max of a NonEmpty always exists. But the min/max of a list can be Nothing.