2The only exception to this semantic equivalence between structured theories and their flattened form is the case in which a theory imports some modules, since any of the protecting or extending initiality requirements of the imported module and its submodules must be preserved. Those requirements would be lost if the whole structure were to be flattened.