Reconciling Lambek's Restriction, Cut-Elimination, and Substitution in the Presence of Exponential Modalities