diff --git a/CHANGELOG.md b/CHANGELOG.md
index fc8d8565ac9df9ecc081ec3f8fc318776c0443fa..0b8390eb46d6d3596a196d69b4399379605e5c15 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -55,6 +55,9 @@ Coq 8.13, 8.14, and 8.15 are no longer supported.
   of `mra R` is designed to embed the preorder relation `R`. (by Amin Timany)
 * Rename instances `union_with_proper` → `union_with_ne`,
   `map_fmap_proper` → `map_fmap_ne`, `map_zip_with_proper` → `map_zip_with_ne`.
+* Rename `dist_option_Forall2` → `option_dist_Forall2`. Add similar lemma
+  `list_dist_Forall2`.
+* Add instances `option_fmap_dist_inj` and `list_fmap_dist_inj`.
 
 **Changes in `bi`:**
 
@@ -237,6 +240,8 @@ s/\bbupd_plain\b/bupd_elim/g
 # Logical atomicity (will break Autosubst notation!)
 s/<<</<<\{/g
 s/>>>/\}>>/g
+# option dist
+s/\bdist_option_Forall2\b/option_dist_Forall2/g
 EOF
 ```
 
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 66a05ce0c13b91a52153732b51f404f05af821ef..d09ab124dfdb1dc1ebf7c035832140d813622ba3 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -9,8 +9,10 @@ Implicit Types l : list A.
 
 Local Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
 
+Lemma list_dist_Forall2 n l k : l ≡{n}≡ k ↔ Forall2 (dist n) l k.
+Proof. done. Qed.
 Lemma list_dist_lookup n l1 l2 : l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
-Proof. setoid_rewrite dist_option_Forall2. apply Forall2_lookup. Qed.
+Proof. setoid_rewrite option_dist_Forall2. apply Forall2_lookup. Qed.
 
 Global Instance cons_ne : NonExpansive2 (@cons A) := _.
 Global Instance app_ne : NonExpansive2 (@app A) := _.
@@ -21,7 +23,7 @@ Global Instance drop_ne n : NonExpansive (@drop A n) := _.
 Global Instance head_ne : NonExpansive (head (A:=A)).
 Proof. destruct 1; by constructor. Qed.
 Global Instance list_lookup_ne i : NonExpansive (lookup (M:=list A) i).
-Proof. intros ????. by apply dist_option_Forall2, Forall2_lookup. Qed.
+Proof. intros ????. by apply option_dist_Forall2, Forall2_lookup. Qed.
 Global Instance list_lookup_total_ne `{!Inhabited A} i :
   NonExpansive (lookup_total (M:=list A) i).
 Proof. intros ???. rewrite !list_lookup_total_alt. by intros ->. Qed.
@@ -31,14 +33,14 @@ Global Instance list_insert_ne i : NonExpansive2 (insert (M:=list A) i) := _.
 Global Instance list_inserts_ne i : NonExpansive2 (@list_inserts A i) := _.
 Global Instance list_delete_ne i : NonExpansive (delete (M:=list A) i) := _.
 Global Instance option_list_ne : NonExpansive (@option_list A).
-Proof. intros ????; by apply Forall2_option_list, dist_option_Forall2. Qed.
+Proof. intros ????; by apply Forall2_option_list, option_dist_Forall2. Qed.
 Global Instance list_filter_ne n P `{∀ x, Decision (P x)} :
   Proper (dist n ==> iff) P →
   Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
 Global Instance replicate_ne n : NonExpansive (@replicate A n) := _.
 Global Instance reverse_ne : NonExpansive (@reverse A) := _.
 Global Instance last_ne : NonExpansive (@last A).
-Proof. intros ????; by apply dist_option_Forall2, Forall2_last. Qed.
+Proof. intros ????; by apply option_dist_Forall2, Forall2_last. Qed.
 Global Instance resize_ne n : NonExpansive2 (@resize A n) := _.
 
 Global Instance cons_dist_inj n :
@@ -132,6 +134,10 @@ Proof.
   induction 1; destruct 1; simpl; [constructor..|f_equiv; try apply Hf; auto].
 Qed.
 
+Global Instance list_fmap_dist_inj {A B : ofe} (f : A → B) n :
+  Inj (≡{n}≡) (≡{n}≡) f → Inj (≡{n}@{list A}≡) (≡{n}@{list B}≡) (fmap f).
+Proof. apply list_fmap_inj. Qed.
+
 Lemma big_opL_ne_2 {M : ofe} {o : M → M → M} `{!Monoid o} {A : ofe} (f g : nat → A → M) l1 l2 n :
   l1 ≡{n}≡ l2 →
   (∀ k y1 y2,
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 99c9f05b1bf7d9de27689f92af270a0f5e77bf1d..00626d4374811548ac4b7b8cffb0026cb5a1b0a9 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1222,7 +1222,7 @@ Section option.
   Context {A : ofe}.
 
   Local Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
-  Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
+  Lemma option_dist_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
   Proof. done. Qed.
 
   Definition option_ofe_mixin : OfeMixin (option A).
@@ -1295,6 +1295,10 @@ Global Instance option_mjoin_ne {A : ofe} n:
   Proper (dist n ==> dist n) (@mjoin option _ A).
 Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
 
+Global Instance option_fmap_dist_inj {A B : ofe} (f : A → B) n :
+  Inj (≡{n}≡) (≡{n}≡) f → Inj (≡{n}@{option A}≡) (≡{n}@{option B}≡) (fmap f).
+Proof. apply option_fmap_inj. Qed.
+
 Lemma fmap_Some_dist {A B : ofe} (f : A → B) (mx : option A) (y : B) n :
   f <$> mx ≡{n}≡ Some y ↔ ∃ x : A, mx = Some x ∧ y ≡{n}≡ f x.
 Proof.
@@ -1330,10 +1334,6 @@ Proof.
     apply optionO_map_ne, oFunctor_map_contractive.
 Qed.
 
-Global Instance option_fmap_dist_inj {A B : ofe} (f : A → B) n :
-  Inj (≡{n}≡) (≡{n}≡) f → Inj (≡{n}@{option A}≡) (≡{n}@{option B}≡) (fmap f).
-Proof. apply option_fmap_inj. Qed.
-
 (** * Later type *)
 (** Note that the projection [later_car] is not non-expansive (see also the
 lemma [later_car_anti_contractive] below), so it cannot be used in the logic.