diff -r f7c5a010115a -r a01ea04aa58f src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Sat Mar 15 20:27:25 2025 +0100
+++ b/src/HOL/Transfer.thy	Sat Mar 15 20:33:19 2025 +0100
@@ -106,6 +106,8 @@
 
 subsection \<open>Predicates on relations, i.e. ``class constraints''\<close>
 
+text \<open>See also \<^const>\<open>Relation.left_unique\<close> and \<^const>\<open>Relation.right_unique\<close>.\<close>
+
 definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
 
@@ -120,9 +122,6 @@
     (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
     (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
 
-lemma left_unique_iff: "left_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R x z)"
-  unfolding Uniq_def left_unique_def by force
-
 lemma left_totalI:
   "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
 unfolding left_total_def by blast
@@ -141,9 +140,6 @@
 lemma bi_unique_iff: "bi_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R x z) \<and> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R z x)"
   unfolding Uniq_def bi_unique_def by force
 
-lemma right_unique_iff: "right_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R z x)"
-  unfolding Uniq_def right_unique_def by force
-
 lemma right_totalI: "(\<And>y. \<exists>x. A x y) \<Longrightarrow> right_total A"
 by(simp add: right_total_def)