src/HOL/Relation.thy

--- a/src/HOL/Relation.thy	Fri Mar 14 18:11:38 2025 +0100
+++ b/src/HOL/Relation.thy	Fri Mar 14 18:13:56 2025 +0100
@@ -477,6 +477,9 @@
 lemma sympD [dest?]: "symp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
   by (rule symD[to_pred])
 
+lemma symp_on_equality[simp]: "symp_on A (=)"
+  by (simp add: symp_on_def)
+
 lemma sym_Int: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)"
   by (fast intro: symI elim: symE)