--- a/src/HOL/Induct/QuoNestedDataType.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Tue Mar 11 10:20:44 2025 +0100
@@ -50,6 +50,7 @@
 
 theorem equiv_exprel: "equiv UNIV exprel"
 proof (rule equivI)
+  show "exprel \<subseteq> UNIV \<times> UNIV" by simp
   show "refl exprel" by (simp add: refl_on_def exprel_refl)
   show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
   show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)