[nextaccountic]

If your language isn't ergonomic then people will not use it (or use it less). Maybe another theorem prover will arise that makes "correct" definitions more ergonomic

Note that the same thing happens in Rust. Rather than putting trait bounds in structs (like struct Aa<T: Something> { .. }, people are encouraged to make the structs more generic (struct Aa<T> { .. }) and put restrictions on impls instead (impl<T: Something> Aa<T> { .. }). The rationale being that this is more ergonomic because it doesn't require you to repeat bounds in places you don't need them, and if every impl requires a Something bound, you will need the bound to make anything with this type (doubly so if the fields of Aa are private and so you need to build one using a method with T: Something)