This MR is one of the steps towards making Iris compatible with transfinite Iris (see simonspies/iris-parametric-index#1) by changing the definition of
Contractive to be compatible with transfinite Iris. This MR tries to be forward compatible with the eventual goal of parameterizing Iris by the stepindex type. As a consequence, it already generalizes
dist_mono and introduces a
stepindex tactic for solving stepindexing related goals.
To simplify backwards compatibility, this MR defines the old version of
dist_later_fin and one can replace where convenient occurrences of
dist_later_fin in projects using Iris. Please let me know what you think of these changes and whether it makes more sense to factor this differently.