section ‹ Shallow Expressions Meta-Theory › theory Shallow_Expressions imports Variables Expressions Unrestriction Substitutions Extension Liberation Quantifiers Collections Named_Expressions Local_State begin end