src/HOL/Transitive_Closure.thy

--- a/src/HOL/Transitive_Closure.thy	Wed Nov 09 16:39:45 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Nov 09 15:37:21 2022 +0100
@@ -82,6 +82,9 @@
 lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>="
   by blast
 
+lemma reflclp_ident_if_reflp[simp]: "reflp R \<Longrightarrow> R\<^sup>=\<^sup>= = R"
+  by (auto dest: reflpD)
+
 
 subsection \<open>Reflexive-transitive closure\<close>