Upstream Contractiveness

To upstream Iris parametric into Iris master, one crucial step will be changing the definition of Contractiveness, more specifically of dist_later. In Iris parametric, dist_later must be defined as dist_later n x y := ∀ m, m ≺ᵢ n → x ≡{m}≡ y to be compatible with transfinite step-indexing.

Lambda Rust and other projects depend on the current (equivalent) definition dist_later n x y := match n with 0 => True | S n => x ≡{n}≡ y end and its reduction behavior. Thus, to stage upstreaming Iris parametric, we pull out changing the definition of dist_later into a separate issue. To simplify backwards compatibility, we define a version of dist_later called dist_later_fin with the match and replace where convenient occurrences of dist_later with dist_later_fin in projects using Iris.