diff --git a/theories/type_systems/systemf_mu/logrel.v b/theories/type_systems/systemf_mu/logrel.v
index 0fceaeb2fc4e6a4b70cbd4c628941415ae3c1790..80924af43086767e54cd15982640cfe87a50bc40 100644
--- a/theories/type_systems/systemf_mu/logrel.v
+++ b/theories/type_systems/systemf_mu/logrel.v
@@ -105,12 +105,11 @@ Equations type_interp (c : type_case) (t : type) δ (k : nat) (v : match c with
 
   type_interp val_case (A → B) δ k v =>
     ∃ x e, v = LamV x e ∧ is_closed (x :b: nil) e ∧
-      (* Slightly weird formulation: for down-closure, we want to quantify over all k' ≤ k --
-        but with that formulation, the termination checker will not be able to see that k' will really be smaller!
-         Thus, we quantify over the difference kd and subtract *)
-      ∀ v' kd,
-        type_interp val_case A δ (k - kd) v' →
-        type_interp expr_case B δ (k - kd) (subst' x (of_val v') e);
+      (* We write ∀ (H:k' ≤ k), .. instead of k' ≤ k → .. due to a longstanding Coq quirk, see
+         https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.60Program.60.20and.20variable.20names/near/404824378 *)
+      ∀ v' k' (H:k' ≤ k),
+        type_interp val_case A δ k' v' →
+        type_interp expr_case B δ k' (subst' x (of_val v') e);
   type_interp val_case (#α) δ k v =>
     (δ α).(sem_type_car) k v;
   type_interp val_case (∀: A) δ k v =>
@@ -120,13 +119,10 @@ Equations type_interp (c : type_case) (t : type) δ (k : nat) (v : match c with
     ∃ v', v = PackV v' ∧
       ∃ τ : sem_type, type_interp val_case A (τ .: δ) k v';
   (** Recursive type case *)
-  (** Defined with two cases: ordinarily, we might require [k > 0] in the body as a guard for the recursive call,
-     but this does not count as a proper guard for termination for Coq -- therefore we handle the 0-case separately.
+  (** By requiring k' < k, we implicitly encode that k > 0
    *)
-  type_interp val_case (μ: A) δ (S k) v =>
-    ∃ v', v = (roll v')%V ∧ is_closed [] v' ∧ ∀ kd, type_interp val_case (A.[μ: A/]%ty) δ (k - kd) v';
-  type_interp val_case (μ: A) δ 0 v =>
-    ∃ v', v = (roll v')%V ∧ is_closed [] v';
+  type_interp val_case (μ: A) δ k v =>
+    ∃ v', v = (roll v')%V ∧ is_closed [] v' ∧ ∀ k' (H:k' < k), type_interp val_case (A.[μ: A/]%ty) δ k' v';
 
   type_interp expr_case t δ k e =>
     ∀ e' n, n < k → red_nsteps n e e' → ∃ v, to_val e' = Some v ∧ type_interp val_case t δ (k - n) v
@@ -182,9 +178,7 @@ Proof.
   - intros (x & e & -> & ? & _). done.
   - intros (v1 & v2 & -> & ? & ?). simpl; apply andb_True; split; eauto.
   - intros [(v' & -> & ?) | (v' & -> & ?)]; simpl; eauto.
-  - destruct k; simp type_interp.
-    + intros (v' & -> & ?); done.
-    + intros (v' & -> & ? & Ha); done.
+  - intros (v' & -> & ? & Ha); done.
 Qed.
 
 
@@ -258,14 +252,8 @@ Proof.
     exists τ. eapply (IH (k, (A, _))); [ dsimpl | done..].
   - (* fun case *)
     destruct Hv as (x & e & -> & ? & Hv). exists x, e. split_and!; [done..| ].
-    intros v' kd Hv'.
-    (* slightly tricky due to the contravariant recursive occurrence *)
-    set (kd' := k - k').
-    specialize (Hv v' (kd + kd')).
-    replace (k - (kd + kd')) with (k' - kd) in Hv by lia.
-    eapply (IH (k' - kd, (B, expr_case))); [ | lia | by eapply Hv].
-    destruct (decide (k' - kd < k)) as [ ? | ?]; first (left; lia).
-    assert (k' - kd = k) as -> by lia. dsimpl.
+    intros v' k'' Hk'' Hv'.
+    apply Hv, Hv'. lia.
   - (* pair case *)
     destruct Hv as (v1 & v2 & -> & Hv1 & Hv2).
     exists v1, v2. split_and!; first done.
@@ -275,16 +263,9 @@ Proof.
     all: exists v'; split; first done.
     all: eapply (IH (k, (_, _))); [ dsimpl | done..].
   - (* rec case *)
-    destruct k; simp type_interp in Hv.
-    { assert (k' = 0) as -> by lia. simp type_interp. }
     destruct Hv as (v' & -> & ? & Hv).
-    destruct k' as [ | k']; simp type_interp.
-    { eauto. }
     exists v'. split_and!; [ done.. | ].
-    intros kd.
-    (* here we crucially use that we can decrease the index *)
-    eapply (IH (k - kd, (A.[(μ: A)%ty/], val_case))); [ | lia | done].
-    left. lia.
+    intros k'' Hk''. apply Hv. lia.
 Qed.
 
 (** We can now derive the two desired lemmas *)
@@ -402,15 +383,15 @@ Section boring_lemmas.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv. eapply forall_proper. intros ?.
       eapply forall_proper. intros ?.
+      eapply forall_proper. intros ?.
       eapply if_iff; by eapply (IH (_, (_, _))); first dsimpl.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
     - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
-    - destruct k; simp type_interp.
-      + done.
-      + f_equiv; intros ?. f_equiv. f_equiv.
-        eapply forall_proper; intros ?.
-        by eapply (IH (_, (_, _))); first dsimpl.
+    - f_equiv; intros ?. f_equiv. f_equiv.
+      eapply forall_proper; intros ?.
+      eapply forall_proper; intros ?.
+      by eapply (IH (_, (_, _))); first dsimpl.
   Qed.
 
 
@@ -440,17 +421,17 @@ Section boring_lemmas.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv. eapply forall_proper. intros ?.
       eapply forall_proper. intros ?.
+      eapply forall_proper. intros ?.
       eapply if_iff; by eapply (IH (_, (_, _))); first dsimpl.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
     - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
-    - destruct k; simp type_interp.
-      + done.
-      + f_equiv; intros ?. f_equiv. f_equiv.
-        eapply forall_proper; intros ?.
-        etransitivity; first eapply (IH (_, (_, _))); first dsimpl.
-        (* NOTE: nice use of asimpl; :-) *)
-        asimpl. done.
+    - f_equiv; intros ?. f_equiv. f_equiv.
+      eapply forall_proper; intros ?.
+      eapply forall_proper; intros ?.
+      etransitivity; first eapply (IH (_, (_, _))); first dsimpl.
+      (* NOTE: nice use of asimpl; :-) *)
+      asimpl. done.
   Qed.
 
 
@@ -488,17 +469,17 @@ Section boring_lemmas.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv. eapply forall_proper. intros ?.
       eapply forall_proper. intros ?.
+      eapply forall_proper. intros ?.
       eapply if_iff; by eapply (IH (_, (_, _))); first dsimpl.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
     - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
-    - destruct k; simp type_interp.
-      + done.
-      + f_equiv; intros ?. f_equiv. f_equiv.
-        eapply forall_proper; intros ?.
-        etransitivity; first eapply (IH (_, (_, _))); first dsimpl.
-        (* NOTE: nice use of asimpl; :-) *)
-        asimpl. done.
+    - f_equiv; intros ?. f_equiv. f_equiv.
+      eapply forall_proper; intros ?.
+      eapply forall_proper; intros ?.
+      etransitivity; first eapply (IH (_, (_, _))); first dsimpl.
+      (* NOTE: nice use of asimpl; :-) *)
+      asimpl. done.
   Qed.
 
 
@@ -636,8 +617,7 @@ Proof.
   intros j' f Hj' Hf.
 
   simp type_interp in Hf. destruct Hf as (x & e & -> & Hcl & Hf).
-  specialize (Hf v 0).
-  replace (j' - 0) with j' in Hf by lia.
+  specialize (Hf v j' (ltac:(lia))).
   eapply expr_det_step_closure.
   { eapply det_step_beta. apply is_val_of_val. }
   eapply expr_rel_mono; last apply Hf; first lia.
@@ -681,8 +661,8 @@ Proof.
     + eapply sem_context_rel_subset in Hctxt; naive_solver.
   }
 
-  intros v' kd Hv'.
-  specialize (Hbody (<[ x := of_val v']> θ) δ (k - kd)).
+  intros v' k' Hk' Hv'.
+  specialize (Hbody (<[ x := of_val v']> θ) δ k').
   simpl. rewrite subst_subst_map.
   2: { by eapply sem_context_rel_closed. }
   apply Hbody.
@@ -722,8 +702,8 @@ Proof.
     + eapply sem_context_rel_subset in Hctxt; naive_solver.
   }
 
-  intros v' kd Hv'.
-  apply (Hbody θ δ (k - kd)).
+  intros v' k' Hk' Hv'.
+  apply (Hbody θ δ k').
   eapply sem_context_rel_mono; last done. lia.
 Qed.
 
@@ -1005,9 +985,9 @@ Proof.
   eapply (sem_val_expr_rel _ _ _ (RollV v)).
 
   specialize (val_rel_is_closed _ _ _ _ Hv) as ?.
-  destruct j as [ | j]; simp type_interp; first by eauto.
+  simp type_interp.
   exists v. split_and!; [done.. | ].
-  intros kd. eapply val_rel_mono; last done. lia.
+  intros k' Hk'. eapply val_rel_mono; last done. lia.
 Qed.
 
 Lemma compat_unroll n Γ e A :
@@ -1023,7 +1003,7 @@ Proof.
   simp type_interp in Hv. destruct Hv as (v' & -> & ? & Hv).
   eapply expr_det_step_closure.
   { simpl. apply det_step_unroll. apply is_val_of_val. }
-  eapply sem_val_expr_rel. apply Hv.
+  eapply sem_val_expr_rel. apply Hv. lia.
 Qed.
 
 Local Hint Resolve compat_var compat_lam_named compat_lam_anon compat_tlam compat_int compat_bool compat_unit compat_if compat_app compat_tapp compat_pack compat_unpack compat_int_binop compat_int_bool_binop compat_unop compat_pair compat_fst compat_snd compat_injl compat_injr compat_case compat_roll compat_unroll: core.
@@ -1091,6 +1071,6 @@ Proof.
   simp type_interp in Hf. destruct Hf as (x & e & -> & Hcl & Hf).
   eapply expr_det_step_closure.
   { apply det_step_beta. apply is_val_of_val. }
-  apply Hf.
+  apply Hf; first lia.
   eapply val_rel_mono; last done. lia.
 Qed.
diff --git a/theories/type_systems/systemf_mu/z_combinator.v b/theories/type_systems/systemf_mu/z_combinator.v
index 4abde6b061b38e4cd11d1bee91a57f9c21fb02fa..962d4837c536c6f06d684f096bb7adc8fe20e3eb 100644
--- a/theories/type_systems/systemf_mu/z_combinator.v
+++ b/theories/type_systems/systemf_mu/z_combinator.v
@@ -12,7 +12,7 @@ Proof.
   { apply (sem_expr_rel_of_val _ _ _ (LamV x e)). lia. }
   intros _. simp type_interp.
   eexists _, _; split_and!; [done | done | ].
-  intros v' kd _. assert (0 - kd = 0) as -> by lia.
+  intros v' kd Hlt _. assert (kd = 0) as -> by lia.
   (* NOTE: this crucially uses that the expression relation at zero is trivial *)
   apply sem_expr_rel_zero_trivial.
 Qed.
@@ -62,7 +62,7 @@ Proof.
 
   apply (sem_val_expr_rel _ _ _ (LamV _ _)).
   simp type_interp. eexists _, _. split_and!; [done |simplify_closed | ].
-  intros v' kd Hv'. simpl. fold g'.
+  intros v' k' Hk' Hv'. simpl. fold g'.
   eapply semantic_app; first last.
   { apply sem_val_expr_rel. done. }
 
@@ -82,7 +82,7 @@ Proof.
     simpl. eapply is_closed_weaken; first done.
     simplify_list_subseteq.
   }
-  intros v2 kd2 Hv2.
+  intros v2 k'' Hk'' Hv2.
 
   set (θ'' := (<[ "x" := of_val v2 ]> $ <["f" := (λ: "x", g' g' "x")]> $ θ)%E).
   replace (subst' "x" _ _) with (subst_map θ'' e).
@@ -104,7 +104,7 @@ Proof.
   apply (sem_context_rel_insert _ _ _ _ (LamV _ _)).
   { eapply sem_expr_rel_lambda_val; first by simplify_closed.
     destruct k.
-    { simpl. replace (0 - kd2) with 0 by lia. apply sem_expr_rel_zero_trivial. }
+    { simpl. replace (k'') with 0 by lia. apply sem_expr_rel_zero_trivial. }
     eapply IH. lia.
     eapply sem_context_rel_mono; last done. lia.
   }
@@ -139,7 +139,7 @@ Proof.
   apply (sem_val_expr_rel _ _ _ (LamV _ _)).
 
   simp type_interp. eexists _, _. split_and!; [done |simplify_closed | ].
-  intros v' kd Hv'. simpl.
+  intros v' k' Hk'' Hv'. simpl.
   eapply semantic_app; first last.
   { apply sem_val_expr_rel. done. }
   simpl. rewrite subst_is_closed_nil; last done.
@@ -151,9 +151,8 @@ Proof.
   }
 
   (* Factor this into a separate lemma ? *)
-  clear Hv' v' HF. generalize (k - kd) => k0.
-  clear kd.
-  induction k0 as [ k0 IH] using lt_wf_ind.
+  clear Hv' v' HF.
+  induction k' as [ k0 IH] using lt_wf_ind.
 
   eapply expr_det_steps_closure.
   { do_det_step. simpl. econstructor. }
@@ -161,16 +160,17 @@ Proof.
 
   simp type_interp. eexists _, _. split_and!; [done | | ].
   { done. }
-  intros vF kd2 Hv2. simpl.
+  intros vF k'3 Hk'3 Hv2. simpl.
   generalize Hv2 => HF.
 
   simp type_interp in Hv2.
   destruct Hv2 as (x & e & -> & ? & Hv2).
   eapply expr_det_steps_closure. { do_det_step. econstructor. }
   eapply (Hv2 (LamV _ _)).
+  { lia. }
 
   simp type_interp. eexists _, _. split_and!; [done |simplify_closed | ].
-  intros v' kd Hv'. simpl.
+  intros v' k'4 Hk'4 Hv'. simpl.
   eapply semantic_app; first last.
   { apply sem_val_expr_rel. done. }
   simpl.
@@ -185,7 +185,7 @@ Proof.
     eapply val_rel_mono; last done. lia.
   }
   destruct k0 as [ | k0]; last (eapply IH; lia).
-  simpl. rewrite Nat.sub_0_l.
+  replace k'4 with 0 by lia.
   eapply sem_expr_rel_zero_trivial.
 Qed.
 
diff --git a/theories/type_systems/systemf_mu_state/logrel.v b/theories/type_systems/systemf_mu_state/logrel.v
index bc3afd733dc3e1d2f3838cdc3dc034ea85d30e5c..7703886a705211e4eb3ba3caf3e1cc66cb14ee14 100644
--- a/theories/type_systems/systemf_mu_state/logrel.v
+++ b/theories/type_systems/systemf_mu_state/logrel.v
@@ -495,12 +495,11 @@ Equations type_interp (c : type_case) (t : type) δ (k : nat) (W : world) (v : m
 
   type_interp val_case (A → B) δ k W v =>
     ∃ x e, v = LamV x e ∧ is_closed (x :b: nil) e ∧
-      (* Slightly weird formulation: for down-closure, we want to quantify over all k' ≤ k --
-        but with that formulation, the termination checker will not be able to see that k' will really be smaller!
-         Thus, we quantify over the difference kd and subtract *)
-      ∀ v' kd W', W' ⊒ W →
-        type_interp val_case A δ (k - kd) W' v' →
-        type_interp expr_case B δ (k - kd) W' (subst' x (of_val v') e);
+      (* We write ∀ (H:k' ≤ k), .. instead of k' ≤ k → .. due to a longstanding Coq quirk, see
+         https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.60Program.60.20and.20variable.20names/near/404824378 *)
+      ∀ v' k' W' (Hk' : k' ≤ k), W' ⊒ W →
+        type_interp val_case A δ k' W' v' →
+        type_interp expr_case B δ k' W' (subst' x (of_val v') e);
   type_interp val_case (#α) δ k W v =>
     (δ α).(sem_type_car) k W v;
   type_interp val_case (∀: A) δ k W v =>
@@ -509,13 +508,10 @@ Equations type_interp (c : type_case) (t : type) δ (k : nat) (W : world) (v : m
   type_interp val_case (∃: A) δ k W v =>
     ∃ v', v = PackV v' ∧
       ∃ τ : sem_type, type_interp val_case A (τ .: δ) k W v';
-  (** Defined with two cases: ordinarily, we might require [k > 0] in the body as a guard for the recursive call,
-     but this does not count as a proper guard for termination for Coq -- therefore we handle the 0-case separately.
+  (** By requiring k' < k, we implicitly encode that k > 0
    *)
-  type_interp val_case (μ: A) δ (S k) W v =>
-    ∃ v', v = (roll v')%V ∧ is_closed [] v' ∧ ∀ kd, type_interp val_case (A.[μ: A/]%ty) δ (k - kd) W v';
-  type_interp val_case (μ: A) δ 0 W v =>
-    ∃ v', v = (roll v')%V ∧ is_closed [] v';
+  type_interp val_case (μ: A) δ k W v =>
+    ∃ v', v = (roll v')%V ∧ is_closed [] v' ∧ ∀ k' (H : k' < k), type_interp val_case (A.[μ: A/]%ty) δ k' W v';
   (** The reference case *)
   type_interp val_case (Ref a) δ k W v =>
       ∃ (l : loc), v = LitV $ LitLoc l ∧ ∃ i INV, W !! i = Some INV ∧
@@ -576,9 +572,7 @@ Proof.
   - intros (x & e & -> & ? & _). done.
   - intros (v1 & v2 & -> & ? & ?). simpl; apply andb_True; split; eauto.
   - intros [(v' & -> & ?) | (v' & -> & ?)]; simpl; eauto.
-  - destruct k; simp type_interp.
-    + intros (v' & -> & ?); done.
-    + intros (v' & -> & ? & Ha); done.
+  - intros (v' & -> & ? & Ha); done.
   - intros (l & -> & _). done.
 Qed.
 
@@ -609,14 +603,12 @@ Proof.
     exists τ. eapply (IH (k, (A, _))); [ dsimpl | done..].
   - (* fun case *)
     destruct Hv as (x & e & -> & ? & Hv). exists x, e. split_and!; [done..| ].
-    intros v' kd W' Hv' Hincl.
+    intros v' k'' W' Hk'' Hv' Hincl.
     (* slightly tricky due to the contravariant recursive occurrence *)
-    set (kd' := k - k').
-    specialize (Hv v' (kd + kd')).
-    replace (k - (kd + kd')) with (k' - kd) in Hv by lia.
-    eapply (IH (k' - kd, (B, expr_case))); [ | lia | by eapply Hv].
-    destruct (decide (k' - kd < k)) as [ ? | ?]; first (left; lia).
-    assert (k' - kd = k) as -> by lia. dsimpl.
+    specialize (Hv v' k'').
+    eapply (IH (k'', (B, expr_case))); [ | lia | eapply Hv; [lia|done..] ].
+    destruct (decide (k'' < k)) as [ ? | ?]; first (left; lia).
+    replace k'' with k by lia. dsimpl.
   - (* pair case *)
     destruct Hv as (v1 & v2 & -> & Hv1 & Hv2).
     exists v1, v2. split_and!; first done.
@@ -626,16 +618,11 @@ Proof.
     all: exists v'; split; first done.
     all: eapply (IH (k, (_, _))); [ dsimpl | done..].
   - (* rec case *)
-    destruct k; simp type_interp in Hv.
-    { assert (k' = 0) as -> by lia. simp type_interp. }
     destruct Hv as (v' & -> & ? & Hv).
-    destruct k' as [ | k']; simp type_interp.
-    { eauto. }
     exists v'. split_and!; [ done.. | ].
-    intros kd.
+    intros k'' Hk'.
     (* here we crucially use that we can decrease the index *)
-    eapply (IH (k - kd, (A.[(μ: A)%ty/], val_case))); [ | lia | done].
-    left. lia.
+    eapply (IH (k'', (A.[(μ: A)%ty/], val_case))); [left | | apply Hv]; lia.
 Qed.
 
 (** We can now derive the two desired lemmas *)
@@ -671,12 +658,13 @@ Proof.
     exists τ. eapply (IH (k, (A, _))); [ dsimpl | done..].
   - (* fun case *)
     destruct Hv as (x & e & -> & ? & Hv). exists x, e. split_and!; [done..| ].
-    intros v' kd W'' Hincl Hv'.
-    specialize (Hv v' kd W'').
-    eapply (IH (k - kd, (B, expr_case))); [ dsimpl | | eapply Hv].
+    intros v' k' W'' Hk' Hincl Hv'.
+    specialize (Hv v' k' W'').
+    eapply (IH (k', (B, expr_case))); [ dsimpl | | eapply Hv].
     + done.
+    + lia.
     + etrans; done.
-    + eapply (IH (k -kd, (A, val_case))); last done; last done. dsimpl.
+    + eapply (IH (k', (A, val_case))); last done; last done. dsimpl.
   - (* pair case *)
     destruct Hv as (v1 & v2 & -> & Hv1 & Hv2).
     exists v1, v2. split_and!; first done.
@@ -686,15 +674,11 @@ Proof.
     all: exists v'; split; first done.
     all: eapply (IH (k, (_, _))); [ dsimpl | done..].
   - (* rec case *)
-    destruct k; simp type_interp in Hv.
-    { simp type_interp. }
     destruct Hv as (v' & -> & ? & Hv).
-    simp type_interp.
     exists v'. split_and!; [ done.. | ].
-    intros kd.
+    intros k' Hk'.
     (* here we crucially use that we can decrease the index *)
-    eapply (IH (k - kd, (A.[(μ: A)%ty/], val_case))); [ | done | done].
-    left. lia.
+    eapply (IH (k', (A.[(μ: A)%ty/], val_case))); [left | done | apply Hv]; lia.
   - (* loc case *)
     destruct Hv as (l & -> & (i & INV & Hlook & Heq)).
     exists l. split; first done.
@@ -856,19 +840,19 @@ Section boring_lemmas.
       intros [|m] ?; simpl; eauto.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv. eapply forall_proper. intros ?.
-      eapply forall_proper. intros ?.
+      eapply forall_proper. intros k'.
       eapply forall_proper. intros W'.
+      eapply forall_proper. intros ?.
       eapply if_iff'; intros.
       eapply if_iff; (eapply (IH (_, (_, _))); first dsimpl).
       all: intros; eapply Hd; etrans; done.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
     - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
-    - destruct k; simp type_interp.
-      + done.
-      + f_equiv; intros ?. f_equiv. f_equiv.
-        eapply forall_proper; intros ?.
-        by eapply (IH (_, (_, _))); first dsimpl.
+    - f_equiv; intros ?. f_equiv. f_equiv.
+      eapply forall_proper; intros k'.
+      eapply forall_proper; intros ?.
+      by eapply (IH (_, (_, _))); first dsimpl.
   Qed.
 
   Lemma type_interp_move_ren :
@@ -900,17 +884,15 @@ Section boring_lemmas.
       intros [|m] ?; simpl; eauto.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv. eapply forall_proper. intros ?.
-      eapply forall_proper. intros ?. eapply forall_proper. intros ?.
+      do 3 (eapply forall_proper; intros ?).
       eapply if_iff; first done. eapply if_iff; by eapply (IH (_, (_, _))); first dsimpl.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
     - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
-    - destruct k; simp type_interp.
-      + done.
-      + f_equiv; intros ?. f_equiv. f_equiv.
-        eapply forall_proper; intros ?.
-        etransitivity; first eapply (IH (_, (_, _))); first dsimpl.
-        asimpl. done.
+    - f_equiv; intros ?. f_equiv. f_equiv.
+      do 2 (eapply forall_proper; intros ?).
+      etransitivity; first eapply (IH (_, (_, _))); first dsimpl.
+      asimpl. done.
   Qed.
 
   Lemma type_interp_move_subst  :
@@ -950,18 +932,15 @@ Section boring_lemmas.
         done.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv. eapply forall_proper. intros ?.
-      eapply forall_proper. intros ?. eapply forall_proper. intros W'.
-      eapply if_iff; first done.
-      eapply if_iff; by eapply (IH (_, (_, _))); first dsimpl.
+      do 3 (eapply forall_proper; intros ?).
+      eapply if_iff; first done. eapply if_iff; by eapply (IH (_, (_, _))); first dsimpl.
     - f_equiv. intros ?. f_equiv. intros ?.
       f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
     - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl.
-    - destruct k; simp type_interp.
-      + done.
-      + f_equiv; intros ?. f_equiv. f_equiv.
-        eapply forall_proper; intros ?.
-        etransitivity; first eapply (IH (_, (_, _))); first dsimpl.
-        asimpl. done.
+    - f_equiv; intros ?. f_equiv. f_equiv.
+      do 2 (eapply forall_proper; intros ?).
+      etransitivity; first eapply (IH (_, (_, _))); first dsimpl.
+      asimpl. done.
   Qed.
 
 
@@ -1103,11 +1082,10 @@ Proof.
   intros j' f W'' Hj' HW' Hf.
 
   simp type_interp in Hf. destruct Hf as (x & e & -> & Hcl & Hf).
-  specialize (Hf v 0).
-  replace (j' - 0) with j' in Hf by lia.
+  specialize (Hf v j').
   eapply expr_det_step_closure.
   { eapply det_step_beta. apply is_val_of_val. }
-  eapply expr_rel_mono_idx; last apply Hf; [lia | reflexivity | ].
+  eapply expr_rel_mono_idx; last apply Hf; [ lia | lia | reflexivity | ].
   eapply val_rel_mono; last done; [lia | done].
 Qed.
 
@@ -1148,8 +1126,8 @@ Proof.
     + eapply sem_context_rel_subset in Hctxt; naive_solver.
   }
 
-  intros v' kd W' Hv' Hincl.
-  specialize (Hbody (<[ x := of_val v']> θ) δ (k - kd) W').
+  intros v' k' W' Hk' Hv' Hincl.
+  specialize (Hbody (<[ x := of_val v']> θ) δ k' W').
   simpl. rewrite subst_subst_map.
   2: { by eapply sem_context_rel_closed. }
   apply Hbody.
@@ -1189,8 +1167,8 @@ Proof.
     + eapply sem_context_rel_subset in Hctxt; naive_solver.
   }
 
-  intros v' kd W' Hv' Hincl.
-  apply (Hbody θ δ (k - kd) W').
+  intros v' k' W' Hk' Hv' Hincl.
+  apply (Hbody θ δ k' W').
   eapply sem_context_rel_mono; [ | done..]. lia.
 Qed.
 
@@ -1478,7 +1456,7 @@ Proof.
     intros j' v W'' Hj' HW' Hv. simpl.
     simp type_interp in Hv. destruct Hv as (x & e' & -> & ? & Hv).
     eapply expr_det_step_closure. { apply det_step_beta. apply is_val_of_val. }
-    apply Hv; first done. eapply val_rel_mono; last done; [lia | done].
+    apply Hv; [lia | done | ]. eapply val_rel_mono; last done; [lia | done].
   - simpl. eapply expr_det_step_closure.
     { apply det_step_caser. apply is_val_of_val. }
     eapply (bind [AppLCtx _]).
@@ -1486,7 +1464,7 @@ Proof.
     intros j' v W'' Hj' HW' Hv. simpl.
     simp type_interp in Hv. destruct Hv as (x & e' & -> & ? & Hv).
     eapply expr_det_step_closure. { apply det_step_beta. apply is_val_of_val. }
-    apply Hv; first done. eapply val_rel_mono; last done; [lia | done].
+    apply Hv; [lia | done | ]. eapply val_rel_mono; last done; [lia | done].
 Qed.
 
 Lemma compat_roll n Γ e A :
@@ -1501,9 +1479,9 @@ Proof.
   eapply (sem_val_expr_rel _ _ _ _ (RollV v)).
 
   specialize (val_rel_is_closed _ _ _ _ _ Hv) as ?.
-  destruct j as [ | j]; simp type_interp; first by eauto.
+  simp type_interp.
   exists v. split_and!; [done.. | ].
-  intros kd. eapply val_rel_mono_idx; last done. lia.
+  intros k' Hk'. eapply val_rel_mono_idx; last done. lia.
 Qed.
 
 Lemma compat_unroll n Γ e A :
@@ -1515,11 +1493,12 @@ Proof.
 
   eapply (bind [UnrollCtx]); first done.
   intros j v W' Hj HW Hv.
-  destruct j as [ | j]; first by apply sem_expr_rel_zero_trivial.
   simp type_interp in Hv. destruct Hv as (v' & -> & ? & Hv).
   eapply expr_det_step_closure.
   { simpl. apply det_step_unroll. apply is_val_of_val. }
-  eapply sem_val_expr_rel. apply Hv.
+  destruct j as [|j].
+  + apply sem_expr_rel_zero_trivial.
+  + eapply sem_val_expr_rel, Hv. lia.
 Qed.
 
 
@@ -1754,6 +1733,6 @@ Proof.
   simp type_interp in Hf. destruct Hf as (x & e & -> & Hcl & Hf).
   eapply expr_det_step_closure.
   { apply det_step_beta. apply is_val_of_val. }
-  apply Hf; first done.
+  apply Hf; [lia | done | ].
   eapply val_rel_mono; [ | done..]. lia.
 Qed.
diff --git a/theories/type_systems/systemf_mu_state/mutbit.v b/theories/type_systems/systemf_mu_state/mutbit.v
index 1899ecf40916a242434f803420136b614404562b..fe7937e0804323f4f8a860875dd0270abd7e63ad 100644
--- a/theories/type_systems/systemf_mu_state/mutbit.v
+++ b/theories/type_systems/systemf_mu_state/mutbit.v
@@ -53,7 +53,7 @@ Proof.
   simp type_interp. eexists _, _. split; first done. split.
   - (* flip *)
     simp type_interp. eexists _, _. split; first done. split; first done.
-    intros v1 kd1 W3 Hincl2 Hv1. simpl.
+    intros v1 k1' W3 Hk1' Hincl2 Hv1. simpl.
     simp type_interp. intros e3 h3 h4 W4 n3 Hincl3 Hsat3 ? Hred.
     eapply (red_nsteps_fill [BinOpLCtx _ (LitV _);IfCtx _ _; IfCtx _ _; AppRCtx _]) in Hred as (n4 & e4 & h5 & ? & Hred_load & Hred).
     eapply (load_nsteps_inv' _ _ _ _ _ _ (λ v, v = #0 ∨ v = #1)) in Hred_load; [ | done | ].
@@ -101,7 +101,7 @@ Proof.
       all: rewrite insert_insert; subst INV; simpl; eauto.
   - (* get *)
     simp type_interp. eexists _, _. split; first done. split; first done.
-    intros v1 kd1 W3 Hincl2 Hv1. simpl.
+    intros v1 k'1 W3 Hk'1 Hincl2 Hv1. simpl.
     simp type_interp. intros e3 h3 h4 W4 n3 Hincl3 Hsat3 ? Hred.
     eapply (red_nsteps_fill [BinOpLCtx _ (LitV _);IfCtx _ _; IfCtx _ _; AppRCtx _]) in Hred as (n4 & e4 & h5 & ? & Hred_load & Hred).
     eapply (load_nsteps_inv' _ _ _ _ _ _ (λ v, v = #0 ∨ v = #1)) in Hred_load; [ | done | ].