diff --git a/CHANGELOG.md b/CHANGELOG.md
index d2bf9c6eef30d7cd20d159900120ac526211e8cc..62d023ca6a1edc4eb460ab17187b0e982dd26220 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,6 +15,19 @@ Coq 8.13 is no longer supported.
 * Add custom entry `dfrac` that can be used for `{dq}` / `â–¡` / `{# q}`
   annotation of connectives with a discardable fraction.
 * Add an RA on the `Z` type of integers, using addition for `â‹…`.
+* Prepare Iris to generalize the type of step-indices. This is a large series of
+  changes; more changes will follow later. More documentation will follow as
+  part of
+  [this merge request](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/888).
+  - Change the definition of `dist_later` to an equivalent definition that is
+    future-proof with respect to general step-indices.
+  - Change the definition of the properties of an `ofe` to be slightly more
+    general and future proof (i.e., change `dist_S` into `dist_lt`).
+  - Adapt `f_contractive` to work with the new definition of `dist_later`.
+    For backwards compatibility for existing developments, the tactic
+    `f_contractive_fin` is provided. It uses the old definition of `dist_later`,
+    now called `dist_later_fin`.
+  (by Michael Sammler, Lennard Gäher, and Simon Spies).
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index 306eb8a8d0530d8b80d757067cf8ff96f10b9029..f595606bf0f10a1384a4dc6543a74c87c57d7412 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -72,7 +72,7 @@ Proof.
         destruct (H2 b) as (c&?&?); eauto. by exists c; split; last etrans.
       * intros a ?. destruct (H2' a) as (b&?&?); auto.
         destruct (H1' b) as (c&?&?); eauto. by exists c; split; last etrans.
-  - intros n x y [??]; split; naive_solver eauto using dist_S.
+  - intros n m x y [??] ?; split; naive_solver eauto using dist_le with si_solver.
 Qed.
 Canonical Structure agreeO := Ofe (agree A) agree_ofe_mixin.
 
@@ -139,7 +139,7 @@ Qed.
 Definition agree_cmra_mixin : CmraMixin (agree A).
 Proof.
   apply cmra_total_mixin; try apply _ || by eauto.
-  - intros n x; rewrite !agree_validN_def; eauto using dist_S.
+  - intros n x; rewrite !agree_validN_def; eauto using dist_le.
   - intros x. apply agree_idemp.
   - intros n x y; rewrite !agree_validN_def /=.
     setoid_rewrite elem_of_app; naive_solver.
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index a8439c9b97666e4e736df0ab1a179aa34220e9e9..7d267442f68db19392306a93c04db752dfd5ca08 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -395,10 +395,10 @@ Proof. intros Hyv [z ?]; ofe_subst y; eauto using cmra_validN_op_l. Qed.
 Lemma cmra_validN_included n x y : ✓{n} y → x ≼ y → ✓{n} x.
 Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
 
-Lemma cmra_includedN_S n x y : x ≼{S n} y → x ≼{n} y.
-Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
 Lemma cmra_includedN_le n n' x y : x ≼{n} y → n' ≤ n → x ≼{n'} y.
-Proof. induction 2; auto using cmra_includedN_S. Qed.
+Proof. by intros [z Hz] ?; exists z; eapply dist_le. Qed.
+Lemma cmra_includedN_S n x y : x ≼{S n} y → x ≼{n} y.
+Proof. intros ?. eapply cmra_includedN_le; [done|lia]. Qed.
 
 Lemma cmra_includedN_l n x y : x ≼{n} x ⋅ y.
 Proof. by exists y. Qed.
diff --git a/iris/algebra/cofe_solver.v b/iris/algebra/cofe_solver.v
index 60da38e9e2ac5a0c61f75f9d7c6678d09b22318c..963129f6601d1d8b46c5850240fb65be017b283f 100644
--- a/iris/algebra/cofe_solver.v
+++ b/iris/algebra/cofe_solver.v
@@ -61,7 +61,7 @@ Proof.
     + by intros X n.
     + by intros X Y ? n.
     + by intros X Y Z ?? n; trans (Y n).
-  - intros k X Y HXY n; apply dist_S.
+  - intros k j X Y HXY Hlt n. apply (dist_le k); [|lia].
     by rewrite -(g_tower X) (HXY (S n)) g_tower.
 Qed.
 Definition T : ofe := Ofe tower tower_ofe_mixin.
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 1696e27be87a8bdac9bfce7e83df6f33604bbee1..8220fa9810bcee75bf9d93d6046d42679ebd36b5 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -71,7 +71,7 @@ Proof.
     + by intros [|a|]; constructor.
     + by destruct 1; constructor.
     + destruct 1; inversion_clear 1; constructor; etrans; eauto.
-  - by inversion_clear 1; constructor; apply dist_S.
+  - by inversion_clear 1; constructor; eauto using dist_le with si_solver.
 Qed.
 Canonical Structure csumO : ofe := Ofe (csum A B) csum_ofe_mixin.
 
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 5ebe71471eb3753baf62181766d389c6e8da86d8..646ea3becac92e49bcddadf8723cd0db1e6af79b 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -21,7 +21,7 @@ Proof.
     + by intros m k.
     + by intros m1 m2 ? k.
     + by intros m1 m2 m3 ?? k; trans (m2 !! k).
-  - by intros n m1 m2 ? k; apply dist_S.
+  - intros n m m1 m2 ? ? k. eauto using dist_le with si_solver.
 Qed.
 Canonical Structure gmapO : ofe := Ofe (gmap K A) gmap_ofe_mixin.
 
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 713bf4b3fe2e7e50557c79c65228925d149c4d3c..f13aaf934dd149cdfaf66c1300778064a2540f7f 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -54,7 +54,7 @@ Proof.
   - intros l k. rewrite equiv_Forall2 -Forall2_forall.
     split; induction 1; constructor; intros; try apply equiv_dist; auto.
   - apply _.
-  - rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
+  - rewrite /dist /list_dist. eauto using Forall2_impl, dist_le with si_solver.
 Qed.
 Canonical Structure listO := Ofe (list A) list_ofe_mixin.
 
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 396e8e6106744884b4a865582a0eb89cc89fdfc9..d3d9d7a005d9a9d3d2166511569e35846ef423e5 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -11,6 +11,22 @@ Set Primitive Projections.
     cases, we do not even need non-expansiveness.
 *)
 
+
+(** The tactic [si_solver] solves goals that are solely concerned with
+    step-indices and their relations (i.e., [0], [S n], [n < m], and [n ≤ m]).
+    Currently, this tactic is just an alias for [lia]. However, in the future,
+    Iris will generalize over the type of step-indices, and this tactic will
+    be able to solve step-indexing goals also in this generalized setting.
+
+    The tactic can be used as part of [eauto] by using the hint database
+    [si_solver].
+*)
+
+Ltac si_solver := lia.
+
+Create HintDb si_solver.
+Global Hint Extern 1 => si_solver : si_solver.
+
 (** Unbundled version *)
 Class Dist A := dist : nat → relation A.
 Global Hint Mode Dist ! : typeclass_instances.
@@ -49,7 +65,7 @@ Tactic Notation "ofe_subst" :=
 Record OfeMixin A `{Equiv A, Dist A} := {
   mixin_equiv_dist (x y : A) : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
   mixin_dist_equivalence n : Equivalence (@dist A _ n);
-  mixin_dist_S n (x y : A) : x ≡{S n}≡ y → x ≡{n}≡ y
+  mixin_dist_lt n m (x y : A) : x ≡{n}≡ y → m < n → x ≡{m}≡ y;
 }.
 
 (** Bundled version *)
@@ -102,8 +118,8 @@ Section ofe_mixin.
   Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
   Global Instance dist_equivalence n : Equivalence (@dist A _ n).
   Proof. apply (mixin_dist_equivalence _ (ofe_mixin A)). Qed.
-  Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y.
-  Proof. apply (mixin_dist_S _ (ofe_mixin A)). Qed.
+  Lemma dist_lt n m x y : x ≡{n}≡ y → m < n → x ≡{m}≡ y.
+  Proof. apply (mixin_dist_lt _ (ofe_mixin A)). Qed.
 End ofe_mixin.
 
 Global Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.
@@ -177,9 +193,11 @@ Section ofe.
   Proof. intros x y Hxy. rewrite /Discrete. by setoid_rewrite Hxy. Qed.
 
   Lemma dist_le n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y.
-  Proof. induction 2; eauto using dist_S. Qed.
+  Proof. intros ? [Hm | ->]%Nat.lt_eq_cases; [by eapply dist_lt | auto]. Qed.
   Lemma dist_le' n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y.
-  Proof. intros; eauto using dist_le. Qed.
+  Proof. eauto using dist_le. Qed.
+  Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y.
+  Proof. eauto using dist_le. Qed.
   (** [ne_proper] and [ne_proper_2] are not instances to improve efficiency of
   type class search during setoid rewriting.
   Local Instances of [NonExpansive{,2}] are hence accompanied by instances of
@@ -209,18 +227,39 @@ Section ofe.
 End ofe.
 
 (** Contractive functions *)
-Definition dist_later `{!Dist A} (n : nat) (x y : A) : Prop :=
-  match n with 0 => True | S n => x ≡{n}≡ y end.
-Global Arguments dist_later _ _ !_ _ _ /.
+(** Defined as a record to avoid eager unfolding. *)
+Record dist_later `{!Dist A} n (x y : A) : Prop :=
+  { dist_later_lt : ∀ m, m < n → x ≡{m}≡ y }.
+
+Section dist_later.
+  Context {A : ofe}.
+  Implicit Types x y : A.
+
+  Global Instance dist_later_equivalence n : Equivalence (@dist_later A _ n).
+  Proof.
+    split.
+    - intros ?; by split.
+    - intros ?? [Hlater]; split; intros ??; by rewrite Hlater.
+    - intros ??? [Hlater1] [Hlater2]; split; intros ??; by rewrite Hlater1 ?Hlater2.
+  Qed.
 
-Global Instance dist_later_equivalence (A : ofe) n : Equivalence (@dist_later A _ n).
-Proof. destruct n as [|n]; [by split|]. apply dist_equivalence. Qed.
+  Lemma dist_dist_later n x y : dist n x y → dist_later n x y.
+  Proof. intros. split; eauto using dist_le. Qed.
 
-Lemma dist_dist_later {A : ofe} n (x y : A) : dist n x y → dist_later n x y.
-Proof. intros Heq. destruct n; first done. exact: dist_S. Qed.
+  Lemma dist_later_dist_lt n m x y : m < n → dist_later n x y → dist m x y.
+  Proof. intros ? []; eauto. Qed.
+
+  Lemma dist_later_0 x y : dist_later 0 x y.
+  Proof. split; intros ? []%Nat.nlt_0_r. Qed.
+
+  Lemma dist_later_S n x y: x ≡{n}≡ y ↔ dist_later (S n) x y.
+  Proof.
+    split.
+    - intros Hn; split; intros m Hm. eapply dist_le; first done. lia.
+    - intros Hdist. apply Hdist. lia.
+  Qed.
+End dist_later.
 
-Lemma dist_later_dist {A : ofe} n (x y : A) : dist_later (S n) x y → dist n x y.
-Proof. done. Qed.
 
 (* We don't actually need this lemma (as our tactics deal with this through
    other means), but technically speaking, this is the reason why
@@ -228,7 +267,28 @@ Proof. done. Qed.
    preserves contractivity. *)
 Lemma ne_dist_later {A B : ofe} (f : A → B) :
   NonExpansive f → ∀ n, Proper (dist_later n ==> dist_later n) f.
-Proof. intros Hf [|n]; last exact: Hf. hnf. by intros. Qed.
+Proof. intros Hf ??? Hlater; split; intros ??; by eapply Hf, Hlater. Qed.
+
+(** We define [dist_later_fin], an equivalent (see dist_later_fin_iff) version of
+   [dist_later] that uses a [match] on the step-index instead of the
+   quantification over smaller step-indicies. The definition of [dist_later_fin]
+   matches how [dist_later] used to be defined (i.e., with a [match] on the
+   step-index), so [dist_later_fin] simplifies adapting existing Iris
+   developments that used to rely on the reduction behavior of [dist_later].
+
+   The "fin" indicates that when, in the future, the step-index is abstracted away,
+   this equivalence will only hold for finite step-indices (as in, ordinals without
+   "limit" steps such as natural numbers).
+*)
+Definition dist_later_fin {A : ofe} (n : nat) (x y : A) :=
+  match n with 0 => True | S n => x ≡{n}≡ y end.
+
+Lemma dist_later_fin_iff {A : ofe} (n : nat) (x y : A):
+  dist_later n x y ↔ dist_later_fin n x y.
+Proof.
+  destruct n; unfold dist_later_fin; first by split; eauto using dist_later_0.
+  by rewrite dist_later_S.
+Qed.
 
 Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f).
 
@@ -241,29 +301,117 @@ Section contractive.
   Implicit Types x y : A.
 
   Lemma contractive_0 x y : f x ≡{0}≡ f y.
-  Proof. by apply (_ : Contractive f). Qed.
-  Lemma contractive_S n x y : x ≡{n}≡ y → f x ≡{S n}≡ f y.
+  Proof. by apply (_ : Contractive f), dist_later_0. Qed.
+  Lemma contractive_dist_later_dist n x y : dist_later n x y → f x ≡{n}≡ f y.
   Proof. intros. by apply (_ : Contractive f). Qed.
+  Lemma contractive_S n x y : x ≡{n}≡ y → f x ≡{S n}≡ f y.
+  Proof. intros. by apply contractive_dist_later_dist, dist_later_S. Qed.
 
   Global Instance contractive_ne : NonExpansive f | 100.
-  Proof. by intros n x y ?; apply dist_S, contractive_S. Qed.
+  Proof. intros n x y ?. eapply contractive_dist_later_dist. by apply dist_dist_later. Qed.
   Global Instance contractive_proper : Proper ((≡) ==> (≡)) f | 100.
   Proof. apply (ne_proper _). Qed.
 End contractive.
 
-Ltac f_contractive :=
+Lemma dist_pointwise_lt {A} {B: ofe} n m (f g: A → B):
+  m < n →
+  pointwise_relation A (dist_later n) f g →
+  pointwise_relation A (dist m) f g.
+Proof. intros Hlt Hp a. by apply Hp. Qed.
+
+(** The tactic [f_contractive] can be used to prove contractiveness or
+    non-expansiveness of a function [f]. Inside of the proof of
+    contractiveness/non-expansiveness, if the current goal is
+      [g x1 ... xn ≡{i}≡ g y1 ... yn]
+    for a contractive function [g] (that is used inside of the body of [f]),
+    then the tactic will try to find a suitable [Contractive] instance for [g]
+    and apply it. Currently, the tactic only supports one (i.e., [n = 1]) and
+    two (i.e., [n = 2]) arguments. As a result of applying the [Contractive]
+    instance for [g], one of the goals will be [dist_later i xi yi] and the tactic
+    will try to simplify or solve the goal. By simplify we mean that it will
+    turn hypotheses [dist_later] into [dist].
+
+    For backwards compatibility, we also define the tactic [f_contractive_fin] that
+    works with an earlier definition of [dist_later] now called [dist_later_fin]. The
+    new version of [f_contractive] is future proof with respect to generalizing the
+    type of step-indices, while the old tactic relies crucially on the step-indices
+    being [nat] and the reduction behavior of [dist_later]. The tactic [f_contractive_fin]
+    simplifies backwards compatibility of existing Iris developments (e.g., RustBelt),
+    that define custom notions of [dist] and [dist_later] but should be avoided if possible.
+
+    The tactics [f_contractive_prepare], [f_contractive_core], and
+    [f_contractive_core_fin] below are internal tactics used to define
+    [f_contractive] and [f_contractive_fin].
+*)
+
+(** [f_contractive_prepare] looks at which function is being applied on both
+    sides of a [dist], looks up the [Contractive] instance (or the equivalent for
+    two arguments) and applies it.
+
+    After applying [f_contractive_prepare], one of the remaining goals is
+    [dist_later n x y] for some [n], [x] and [y]. At this point, one of two
+    tactics can be applied: [f_contractive_core] or [f_contractive_core_fin]. The
+    tactic [f_contractive_core] works with the normal definition of [dist_later]
+    and is future compatible with generalizing the step-index beyond natural
+    numbers. The tactic [f_contractive_core_fin] is a special case which only
+    works for natural numbers as step-indicies. It changes [dist_later] to
+    [dist_later_fin], which only makes sense on natural numbers. We keep
+    [f_contractive_core_fin] around for backwards compatibility.
+*)
+Ltac f_contractive_prepare :=
   match goal with
   | |- ?f _ ≡{_}≡ ?f _ => simple apply (_ : Proper (dist_later _ ==> dist _) f)
   | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (dist_later _ ==> _ ==> dist _) f)
   | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (_ ==> dist_later _ ==> dist _) f)
-  end;
+  end.
+
+(** For the goal [dist_later n x y], the tactic [f_contractive_core] introduces a
+    smaller step-index [m < n] and tries to lower assumptions in the context to
+    [m] where possible.
+*)
+Ltac f_contractive_core idxName ltName :=
+  try match goal with
+  | |- dist_later ?n ?x ?y =>
+      constructor; intros idxName ltName;
+      repeat match goal with
+      | H: dist_later n _ _ |- _ => destruct H as [H]; specialize (H idxName ltName) as H
+      | H: pointwise_relation _ (dist_later n) _ _ |- _ =>
+         apply (dist_pointwise_lt _ idxName _ _ ltName) in H
+      end
+  end.
+
+(** For the goal [dist_later n x y], the tactic [f_contractive_core_fin] changes
+    the goal to [dist_later_fin] and takes care of the case where [n=0], such
+    that we are only left with the case where [n = S n'] for some [n']. Changing
+    [dist_later] to [dist_later_fin] enables reduction and thus works better with
+    custom versions of [dist] as used e.g. by LambdaRust. *)
+Ltac f_contractive_core_fin :=
   try match goal with
   | |- @dist_later ?A _ ?n ?x ?y =>
-         destruct n as [|n]; [exact I|change (@dist A _ n x y)]
-  end;
-  (* Only try reflexivity if the terms are syntactically equal. This avoids
-     very expensive failing unification. *)
-  try match goal with  |- _ ?x ?x => simple apply reflexivity end.
+      apply dist_later_fin_iff;
+      destruct n as [|n]; [exact I|change (@dist A _ n x y)]
+  end.
+
+
+(** We combine [f_contractive_prepare] and [f_contractive_core] into the
+    [f_contractive] tactic.
+
+    For all the goals not solved by [f_contractive_core] (i.e., the ones that are
+    not [dist_later n x y]), we try reflexivity. Since reflexivity can be very
+    expensive when unification fails, we use [fast_reflexivity].
+*)
+
+Tactic Notation "f_contractive" "as" ident(idxName) ident(ltName) :=
+  f_contractive_prepare; f_contractive_core idxName ltName; try fast_reflexivity.
+
+Tactic Notation "f_contractive" :=
+  let m := fresh "m" in
+  let Hlt := fresh "Hlt" in
+  f_contractive as m Hlt.
+
+Tactic Notation "f_contractive_fin" :=
+  f_contractive_prepare; f_contractive_core_fin; try fast_reflexivity.
+
 
 Ltac solve_contractive :=
   solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]).
@@ -368,7 +516,7 @@ Section fixpoint.
   Proof.
     rewrite !equiv_dist=> Hx n. induction n as [|n IH]; simpl in *.
     - rewrite Hx fixpoint_unfold; eauto using contractive_0.
-    - rewrite Hx fixpoint_unfold. apply (contractive_S _), IH.
+    - rewrite Hx fixpoint_unfold. eauto using contractive_S.
   Qed.
 
   Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
@@ -377,7 +525,7 @@ Section fixpoint.
     intros Hfg. rewrite fixpoint_unseal /fixpoint_def
       (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
     induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
-    rewrite Hfg; apply contractive_S, IH; auto using dist_S.
+    rewrite Hfg; apply contractive_S, IH; eauto using dist_le with si_solver.
   Qed.
   Lemma fixpoint_proper (g : A → A) `{!Contractive g} :
     (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g.
@@ -392,7 +540,7 @@ Section fixpoint.
     intros ? [x Hx] Hincr Hlim. set (chcar i := Nat.iter (S i) f x).
     assert (Hcauch : ∀ n i : nat, n ≤ i → chcar i ≡{n}≡ chcar n).
     { intros n. rewrite /chcar. induction n as [|n IH]=> -[|i] //=;
-        eauto using contractive_0, contractive_S with lia. }
+        eauto using contractive_0, contractive_S with si_solver. }
     set (fp2 := compl {| chain_cauchy := Hcauch |}).
     assert (f fp2 ≡ fp2).
     { apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar.
@@ -504,11 +652,13 @@ Section fixpointAB.
 
   Local Instance: Proper ((≡) ==> (≡) ==> (≡)) fA.
   Proof using fA_contractive.
-    apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
+    apply ne_proper_2=> n x x' ? y y' ?. f_contractive;
+      eauto using dist_le with si_solver.
   Qed.
   Local Instance: Proper ((≡) ==> (≡) ==> (≡)) fB.
   Proof using fB_contractive.
-    apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
+    apply ne_proper_2=> n x x' ? y y' ?. f_contractive;
+      eauto using dist_le with si_solver.
   Qed.
 
   Lemma fixpoint_A_unique p q : fA p q ≡ p → fB p q ≡ q → p ≡ fixpoint_A.
@@ -541,7 +691,7 @@ Section fixpointAB_ne.
     fixpoint_B fA fB ≡{n}≡ fixpoint_B fA' fB'.
   Proof.
     intros HfA HfB. apply fixpoint_ne=> z. rewrite HfB. f_contractive.
-    apply fixpoint_A_ne; auto using dist_S.
+    apply fixpoint_A_ne; eauto using dist_le with si_solver.
   Qed.
 
   Lemma fixpoint_A_proper :
@@ -582,7 +732,7 @@ Section ofe_mor.
       + by intros f x.
       + by intros f g ? x.
       + by intros f g h ?? x; trans (g x).
-    - by intros n f g ? x; apply dist_S.
+    - intros n m f g ? x ?; eauto using dist_le with si_solver.
   Qed.
   Canonical Structure ofe_morO := Ofe (ofe_mor A B) ofe_mor_ofe_mixin.
 
@@ -690,7 +840,8 @@ Section product.
     - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
       rewrite !equiv_dist; naive_solver.
     - apply _.
-    - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
+    - by intros n m [x1 y1] [x2 y2] [??] ?; split;
+        eauto using dist_le with si_solver.
   Qed.
   Canonical Structure prodO : ofe := Ofe (A * B) prod_ofe_mixin.
 
@@ -878,7 +1029,9 @@ Global Instance ofe_morOF_contractive F1 F2 :
   oFunctorContractive (ofe_morOF F1 F2).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
-  apply ofe_morO_map_ne; apply oFunctor_map_contractive; destruct n, Hfg; by split.
+  apply ofe_morO_map_ne; apply oFunctor_map_contractive;
+    split; intros m Hlt; split; simpl.
+  all: destruct Hfg as [Hfg]; destruct (Hfg m); auto.
 Qed.
 
 (** * Sum type *)
@@ -898,7 +1051,7 @@ Section sum.
       + destruct Hx=> n; constructor; by apply equiv_dist.
       + destruct (Hx 0); constructor; apply equiv_dist=> n; by apply (inj _).
     - apply _.
-    - destruct 1; constructor; by apply dist_S.
+    - destruct 1; constructor; eapply dist_lt; eauto.
   Qed.
   Canonical Structure sumO : ofe := Ofe (A + B) sum_ofe_mixin.
 
@@ -918,7 +1071,7 @@ Section sum.
     { compl := sum_compl }.
   Next Obligation.
     intros ?? n c; rewrite /compl /sum_compl.
-    feed inversion (chain_cauchy c 0 n); first by auto with lia; constructor.
+    feed inversion (chain_cauchy c 0 n); first by si_solver.
     - rewrite (conv_compl n (inl_chain c _)) /=. destruct (c n); naive_solver.
     - rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver.
   Qed.
@@ -1074,7 +1227,7 @@ Section option.
       intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist.
       by intros n; feed inversion (Hxy n).
     - apply _.
-    - destruct 1; constructor; by apply dist_S.
+    - destruct 1; constructor; eauto using dist_le with si_solver.
   Qed.
   Canonical Structure optionO := Ofe (option A) option_ofe_mixin.
 
@@ -1192,14 +1345,13 @@ Section later.
   Proof.
     split.
     - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
-      split.
-      + intros Hxy [|n]; [done|apply Hxy].
-      + intros Hxy n; apply (Hxy (S n)).
+      split; intros Hxy n; [done|].
+      eapply (Hxy (S n)). lia.
     - split; rewrite /dist /later_dist.
       + by intros [x].
       + by intros [x] [y].
       + by intros [x] [y] [z] ??; trans y.
-    - intros [|n] [x] [y] ?; [done|]; rewrite /dist /later_dist; by apply dist_S.
+    - intros n m [x] [y] Hdist ?; split; intros p Hp. eapply Hdist; by trans m.
   Qed.
   Canonical Structure laterO : ofe := Ofe (later A) later_ofe_mixin.
 
@@ -1209,12 +1361,13 @@ Section later.
   Global Program Instance later_cofe `{Cofe A} : Cofe laterO :=
     { compl c := Next (compl (later_chain c)) }.
   Next Obligation.
-    intros ? [|n] c; [done|by apply (conv_compl n (later_chain c))].
+    intros ? n c. apply dist_later_fin_iff.
+    destruct n as [|n]; [done|by apply (conv_compl n (later_chain c))].
   Qed.
 
   Global Instance Next_contractive : Contractive (@Next A).
-  Proof. by intros [|n] x y. Qed.
-  Global Instance Next_inj n : Inj (dist n) (dist (S n)) (@Next A).
+  Proof. by intros n x y. Qed.
+  Global Instance Next_inj n : Inj (dist_later n) (dist n) (@Next A).
   Proof. by intros x y. Qed.
 
   Lemma Next_uninj x : ∃ a, x ≡ Next a.
@@ -1239,9 +1392,18 @@ Global Arguments laterO : clear implicits.
 Definition later_map {A B} (f : A → B) (x : later A) : later B :=
   Next (f (later_car x)).
 Global Instance later_map_ne {A B : ofe} (f : A → B) n :
-  Proper (dist (pred n) ==> dist (pred n)) f →
+  Proper (dist_later n ==> dist_later n) f →
   Proper (dist n ==> dist n) (later_map f) | 0.
-Proof. destruct n as [|n]; intros Hf [x] [y] ?; do 2 red; simpl; auto. Qed.
+Proof.
+  intros P [x] [y] Hdist; rewrite /later_map //=.
+  split; intros m Hm; apply P, Hm. apply Hdist.
+Qed.
+Global Instance later_map_ne' {A B : ofe} (f : A → B) `{NonExpansive f} :
+  NonExpansive (later_map f).
+Proof.
+  intros ? [x] [y] Hdist. unfold later_map; simpl.
+  split; intros ??; simpl. f_equiv. by eapply Hdist.
+Qed.
 Global Instance later_map_proper {A B : ofe} (f : A → B) :
   Proper ((≡) ==> (≡)) f →
   Proper ((≡) ==> (≡)) (later_map f).
@@ -1257,7 +1419,7 @@ Proof. destruct x; intros Hf; apply Hf. Qed.
 Definition laterO_map {A B} (f : A -n> B) : laterO A -n> laterO B :=
   OfeMor (later_map f).
 Global Instance laterO_map_contractive (A B : ofe) : Contractive (@laterO_map A B).
-Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
+Proof. intros n f g Hlater [x]; split; intros ??; simpl. by apply Hlater. Qed.
 
 Program Definition laterOF (F : oFunctor) : oFunctor := {|
   oFunctor_car A _ B _ := laterO (oFunctor_car F A B);
@@ -1280,7 +1442,7 @@ Notation "â–¶ F"  := (laterOF F%OF) (at level 20, right associativity) : oFuncto
 Global Instance laterOF_contractive F : oFunctorContractive (laterOF F).
 Proof.
   intros A1 ? A2 ? B1 ? B2 ? n fg fg' Hfg. apply laterO_map_contractive.
-  destruct n as [|n]; simpl in *; first done. apply oFunctor_map_ne, Hfg.
+  split; intros ???; simpl. by eapply oFunctor_map_ne, Hfg.
 Qed.
 
 (** * Dependently-typed functions over a discrete domain *)
@@ -1314,7 +1476,7 @@ Section discrete_fun.
       + by intros f x.
       + by intros f g ? x.
       + by intros f g h ?? x; trans (g x).
-    - by intros n f g ? x; apply dist_S.
+    - by intros n m f g ? ? x; eauto using dist_le with si_solver.
   Qed.
   Canonical Structure discrete_funO := Ofe (discrete_fun B) discrete_fun_ofe_mixin.
 
@@ -1407,7 +1569,7 @@ Proof.
     + intros y. by apply g_dist.
     + intros y1 y2. by rewrite !g_dist.
     + intros y1 y2 y3. rewrite !g_dist. intros ??; etrans; eauto.
-  - intros n y1 y2. rewrite !g_dist. apply dist_S.
+  - intros n m y1 y2. rewrite !g_dist. eauto using dist_le with si_solver.
 Qed.
 
 Section iso_cofe_subtype.
@@ -1525,8 +1687,8 @@ Section sigT.
         destruct 1 as [-> Heq1].
         destruct 1 as [-> Heq2]. exists eq_refl => /=. by trans y.
     - setoid_rewrite sigT_dist_eq.
-      move => [xa x] [ya y] /=. destruct 1 as [-> Heq].
-      exists eq_refl. exact: dist_S.
+      move => m [xa x] [ya y] /=. destruct 1 as [-> Heq].
+      exists eq_refl. by eapply dist_dist_later.
   Qed.
 
   Canonical Structure sigTO : ofe := Ofe (sigT P) sigT_ofe_mixin.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index baf5a62335ae28ec400cd395eaa703f23051c45a..cdc2b6425096d3c045b243da0fc86e521aa35707 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -232,7 +232,7 @@ Section cmra.
       intros [[[dq aa]|] b]; rewrite /= ?cmra_valid_validN; naive_solver.
     - rewrite view_validN_eq=> n [[[dq ag]|] b] /=.
       + intros [? (a&?&?)]; split; [done|].
-        exists a; split; [by eauto using dist_S|].
+        exists a; split; [by eauto using dist_le|].
         apply view_rel_mono with (S n) a b; auto with lia.
       + intros [a ?]. exists a. apply view_rel_mono with (S n) a b; auto with lia.
     - rewrite view_validN_eq=> n [[[q1 ag1]|] b1] [[[q2 ag2]|] b2] /=.
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index 318fd089f8b318cac2c62a933811338ff365e521..c92fdb22240c2d0d563b377227b6c2e32eb588a5 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -167,7 +167,7 @@ Module le_upd.
     Proof.
       intros n; induction (lt_wf n) as [n _ IH].
       intros P1 P2 HP. rewrite (le_upd_unfold P1) (le_upd_unfold P2).
-      do 9 (done || f_equiv). f_contractive. eapply IH, dist_S; [lia|done].
+      do 9 (done || f_equiv). f_contractive. eapply IH, dist_le; [lia|done|lia].
     Qed.
 
     Lemma bupd_le_upd P : (|==> P) -∗ (|==£> P).
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 1c274a2a498678b910753c1c539aab3c1da07198..a1a1bb2378fad8583936480d1e2ba1855d0c72e5 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -138,7 +138,7 @@ Section cofe.
       + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
       + intros P Q Q' HP HQ; split=> i x ??.
         by trans (Q i x);[apply HP|apply HQ].
-    - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
+    - intros n m P Q HPQ Hlt. split=> i x ??; apply HPQ; eauto with lia.
   Qed.
   Canonical Structure uPredO : ofe := Ofe (uPred M) uPred_ofe_mixin.
 
@@ -242,7 +242,9 @@ Global Instance uPredOF_contractive F :
   urFunctorContractive F → oFunctorContractive (uPredOF F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
-  apply uPredO_map_ne, urFunctor_map_contractive. destruct n; split; by apply HPQ.
+  apply uPredO_map_ne, urFunctor_map_contractive.
+  destruct HPQ as [HPQ]. constructor. intros ??.
+  split; by eapply HPQ.
 Qed.
 
 (** logical entailement *)
@@ -551,7 +553,7 @@ Section primitive.
   Lemma later_contractive : Contractive (@uPred_later M).
   Proof.
     unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try lia.
-    apply HPQ; eauto using cmra_validN_S.
+    eapply HPQ; eauto using cmra_validN_S.
   Qed.
 
   Lemma plainly_ne : NonExpansive (@uPred_plainly M).
@@ -787,9 +789,16 @@ Section primitive.
   Proof. by unseal. Qed.
 
   Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
-  Proof. by unseal. Qed.
+  Proof.
+    unseal. split. intros [|n]; simpl; [done|].
+    intros ?? Heq; apply Heq; auto.
+  Qed.
   Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
-  Proof. by unseal. Qed.
+  Proof.
+    unseal. split. intros n ? ? Hn; split; intros m Hlt; simpl in *.
+    destruct n as [|n]; first lia.
+    eauto using dist_le with si_solver.
+  Qed.
 
   Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
   Proof.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index fc12397c1080cdd411ce51c1c15dd0c7302ef410..07bbb2da3d1d8687bee10052913dcbd20f0b39a0 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -124,7 +124,7 @@ Proof.
   (* FIXME : simplify this proof once we have a good definition and a
      proper instance for step_fupdN. *)
   induction num_laters_per_step as [|k IHk]; simpl; last by rewrite IHk.
-  rewrite IH; [done|lia|]. intros v. eapply dist_S, HΦ.
+  rewrite IH; [done|lia|]. intros v. eapply dist_le; [apply HΦ|lia].
 Qed.
 Global Instance wp_proper s E e :
   Proper (pointwise_relation _ (≡) ==> (≡)) (wp (PROP:=iProp Σ) s E e).
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index 16a80ebe14815da45480d0fd9492a741ec58f4d1..6b1fb69eadce5eb5fd8a24923dcc713fd84face9 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -33,7 +33,7 @@ Section cofe.
       + by intros P Q HPQ; split=> i ?; symmetry; apply HPQ.
       + intros P Q Q' HP HQ; split=> i ?.
         by trans (Q i);[apply HP|apply HQ].
-    - intros n P Q HPQ; split=> i ?; apply HPQ; auto.
+    - intros n m P Q HPQ Hlt. split=> i ?; apply HPQ; lia.
   Qed.
   Canonical Structure siPropO : ofe := Ofe siProp siProp_ofe_mixin.
 
@@ -199,7 +199,7 @@ Section primitive.
   Lemma later_contractive : Contractive siProp_later.
   Proof.
     unseal; intros [|n] P Q HPQ; split=> -[|n'] ? //=; try lia.
-    apply HPQ; lia.
+    eapply HPQ; eauto with si_solver.
   Qed.
   Lemma internal_eq_ne (A : ofe) : NonExpansive2 (@siProp_internal_eq A).
   Proof.
@@ -281,9 +281,15 @@ Section primitive.
 
   (** Later *)
   Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
-  Proof. by unseal. Qed.
+  Proof.
+    unseal. split. intros [|n]; simpl; [done|].
+    intros Heq; apply Heq; auto.
+  Qed.
   Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
-  Proof. by unseal. Qed.
+  Proof.
+    unseal. split. intros n Hn; split; intros m Hlt; simpl in *.
+    destruct n as [|n]; eauto using dist_le with si_solver.
+  Qed.
 
   Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
   Proof. unseal=> HP; split=>-[|n]; [done|apply HP; eauto using cmra_validN_S]. Qed.