diff -r a718547c3493 -r 855b5f0456d8 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Nov 09 16:45:12 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Nov 09 16:39:45 2022 +0100
@@ -70,6 +70,9 @@
 lemma refl_reflcl[simp]: "refl (r\<^sup>=)"
   by (simp add: refl_on_def)
 
+lemma reflp_on_reflclp[simp]: "reflp_on A R\<^sup>=\<^sup>="
+  by (simp add: reflp_on_def)
+
 lemma antisym_reflcl[simp]: "antisym (r\<^sup>=) = antisym r"
   by (simp add: antisym_def)