Add suggested test

tests/algebra.v

 From iris.algebra Require Import auth excl lib.gmap_view.
 From iris.base_logic.lib Require Import invariants.
 
+Section test_dist_equiv_mode.
+  Local Unset Mangle Names.
+  (* check that the mode for [Dist] does not trigger https://github.com/coq/coq/issues/14441.
+  From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
+
+  (* succeeds *)
+  Lemma list_dist_lookup {A : ofe} n (l1 l2 : list A) :
+    l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
+  Abort.
+  Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) :
+    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
+  Abort.
+  Lemma list_equiv_lookup_equiv `{Equiv A} (l1 l2 : list A) :
+    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
+  Abort.
+
+  Local Hint Mode Equiv ! : typeclass_instances.
+
+  (* succeeds *)
+  Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) :
+    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
+  Abort.
+
+  (* fails *)
+  Fail Lemma list_equiv_lookup_equiv `{Equiv A} (l1 l2 : list A) :
+    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
+End test_dist_equiv_mode.
+
 (** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
 with carriers that are definitionally equal. See also
 https://gitlab.mpi-sws.org/iris/iris/issues/299 *)