add lemmas `intuitionistic` and `intuitionistically_intro`

We have persistently_intro' and persistently_intro, but for the intuitionistic modality we lacked the second lemma.

Also, I recently was looking for a lemma like intuitionistic and did not find it. I now realize intuitionistic_intuitionistically would have done it, but given that we have persistent as a lemma (the projection of the Persistent class), I think it makes sense to also have intuitionistic.