In Frederic Fitch's Symbolic Logic he proves (11.8, page 66) that "◻p" coimplicates "◻◻p".
In 11.10 (page 66), he writes,
A system almost the same as the system Lewis calls S2 is obtainable by adding the principle of excluded middle to the present system and making a restriction as follows: When reiterating into a strict subordinate proof, the first square on the left side of the reiterated proposition must be dropped and only the remaining part of the proposition written as an item of the subordinate proof. This restriction would make it impossible to prove [◻p ⊃ ◻◻p] in general, and the second subordinate proof of 11.8 would be invalid.
By "Lewis" he refers to Lewis and Langford's book Symbolic Logic. The system Fitch presents in his book does not allow the use of the law of excluded middle to apply to an arbitrary proposition, but only to propositions with a definite truth value. This is because he also includes propositions that are "indefinite", that is, without a specific truth value.
This makes me wonder why modal logic needs to use "◻◻p" at all?