Improve naming of lemmas about modalities

The following discussion from !130 (merged) should be addressed:

We agreed on the following scheme

M1_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2_{swap,comm}: M1 (M2 P) ⊣⊢ M2 (M1 P)

However, @robbertkrebbers noted that we have plenty of lemmas of the last form. Optimizing for conciseness, we could also use

M1_{into,impl,entails}_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)