--- a/src/HOL/Library/RBT.thy	Sat May 24 09:06:26 2025 +0200
+++ b/src/HOL/Library/RBT.thy	Wed May 28 17:49:22 2025 +0200
@@ -169,6 +169,10 @@
   "lookup t = Map.empty \<longleftrightarrow> t = empty"
   by transfer (rule RBT_lookup_empty)
 
+lemma keys_empty_eq [simp]:
+  \<open>keys empty = []\<close>
+  by transfer simp
+
 lemma sorted_keys [iff]:
   "sorted (keys t)"
   by transfer (simp add: RBT_Impl.keys_def rbt_sorted_entries)