diff -r cd2521e39783 -r f575ad8dcbe5 src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Wed Jan 15 13:53:03 2025 +0100
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Wed Jan 15 13:53:25 2025 +0100
@@ -322,7 +322,7 @@
   shows "P a"
   by (induct rule: well_order_induct) (rule assms, simp add: underS_def)
 
-lemma suc_underS:
+lemma suc_underS':
   assumes B: "B \<subseteq> Field r" and A: "AboveS B \<noteq> {}" and b: "b \<in> B"
   shows "b \<in> underS (suc B)"
   using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto