diff --git a/theories/Unicode/Utf8.v b/theories/Unicode/Utf8.v
index e07cbb5bbc..d8e7b3926d 100644
--- a/theories/Unicode/Utf8.v
+++ b/theories/Unicode/Utf8.v
@@ -19,6 +19,7 @@ Notation "x ≥ y" := (ge x y) (at level 70, no associativity).
 (*
 Check ∀ x z, True -> (∃ y v, x + v ≥ y + z) ∨ x ≤ 0.
 *)
+(* Check ∀ P, P ↔︎ P. *)
 
 (* Integer Arithmetic *)
 (* TODO: this should come after ZArith
diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v
index ec63022004..dc84783fd7 100644
--- a/theories/Unicode/Utf8_core.v
+++ b/theories/Unicode/Utf8_core.v
@@ -24,7 +24,11 @@ Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope.
 Notation "x → y" := (x -> y)
   (at level 99, y at level 200, right associativity): type_scope.
 
+(* The two following differ in that the second symbol "↔︎" is the
+  symbol "↔" from the first line, appended with
+  the _text variation selector_, indicating that it must be displayed as text and not emoji. *)
 Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope.
+Notation "x ↔︎ y" := (x <-> y) (at level 95, no associativity, only parsing): type_scope.
 Notation "¬ x" := (~x) (at level 75, right associativity) : type_scope.
 Notation "x ≠ y" := (x <> y) (at level 70) : type_scope.