This should fix iris-examples.

Special proof mode class for adding a modality to a goal

See merge request FP/iris-coq!107

This used to be done by using `ElimModal` in backwards direction. Having
a separate type class for this gets rid of some hacks:

- Both `Hint Mode`s in forward and backwards direction for `ElimModal`.
- Weird type class precedence hacks to make sure the right instance is picked.
  These were needed because using `ElimModal` in backwards direction caused
  ambiguity.

This was an oversight in !63.

Consistent handling of pure implication and forall

Closes #127

See merge request FP/iris-coq!104