[pshirshov]

This is not correct.

Not all the options are equal.

It's possible to soundly define, verify and instantiate big modular contexts.

https://github.com/7mind/izumi/

[sokoloff]

Things that are possible are frequently not the default condition.

[pshirshov]

What forces you to stick to the suboptimal "defaults"?