derived_laws.v is a very-hard-to-navigate monster. Can we find a good way to split it?
One fairly obvious thing to do is to split the
Sbi stuff into a separate file. Then the
Bi file will still be huge, probably... what could be a good criterion to separate that?