diff --git a/theories/finite.v b/theories/finite.v
index 93292786559530c92e814131e793a05052b0ccb9..d6ef2254b6d855a04bbfc12b19e7b20256dd8f74 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -208,7 +208,7 @@ Section enc_finite.
     apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj.
     destruct (seq _ _ !! i) as [i'|] eqn:Hi',
       (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_eq/=.
-    destruct (lookup_seq_inv _ _ _ _ Hi'), (lookup_seq_inv _ _ _ _ Hj'); subst.
+    apply lookup_seq in Hi' as  [-> ?]. apply lookup_seq in Hj' as [-> ?].
     rewrite <-(to_of_nat i), <-(to_of_nat j) by done. by f_equal.
   Qed.
   Next Obligation.
diff --git a/theories/list.v b/theories/list.v
index 03660b3fb5bfbb33631285ecb312677e894ec370..4d70d994a406b51bb8db7693e88783d951f8058d 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3725,7 +3725,8 @@ Section seqZ.
     Forall P (seqZ m n) ↔ ∀ m', m ≤ m' < m + n → P m'.
   Proof.
     rewrite Forall_lookup. split.
-    - intros H j [??]. apply (H (Z.to_nat (j - m))), lookup_seqZ. lia.
+    - intros H j [??]. apply (H (Z.to_nat (j - m))), lookup_seqZ.
+      rewrite !Z2Nat.id by lia. lia.
     - intros H j x [-> ?]%lookup_seqZ. auto with lia.
   Qed.
 End seqZ.