WIP: Changing the definition of contractiveness to be compatible with Transfinite Iris

This merge request is a first step towards generalising Iris such that large parts of its definition can be shared with Transfinite Iris. This merge request changes the definition of dist_later such that it generalizes beyond natural numbers.

Specifically, the original definition: dist_later n x y := match n with 0 => True | S n => x ≡{n}≡ y end is replaced with the equivalent definition: dist_later n x y := ∀ m, m < n → x ≡{m}≡ y

The change should be mostly local to the model of Iris with the exception of f_contractive and solve_contractive which are used throughout Iris (and beyond). The merge request provides alternative implementations which can handle the new definition of dist_later.