The *empty* message in the lemma must be revised.
The empty message in the lemma must be revised.