
diff -r fba16c509af0 -r e8c96013ea8a src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/List.thy	Tue Mar 11 10:20:44 2025 +0100
@@ -7647,7 +7647,7 @@
 qed
 
 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
-  by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans)
+  by (simp add: equiv_def listrel_subset listrel_refl_on listrel_sym listrel_trans)
 
 lemma listrel_rtrancl_refl[iff]: "(xs,xs) \<in> listrel(r\<^sup>*)"
   using listrel_refl_on[of UNIV, OF refl_rtrancl]




