src/HOL/Algebra/Coset.thy

    shows "equiv (carrier G) (rcong H)"
 proof -
   interpret group G by fact
   show ?thesis
   proof (intro equivI)
-    show "refl_on (carrier G) (rcong H)"
+    have "rcong H \<subseteq> carrier G \<times> carrier G"
+      by (auto simp add: r_congruent_def)
+    thus "refl_on (carrier G) (rcong H)"
       by (auto simp add: r_congruent_def refl_on_def)
   next
     show "sym (rcong H)"
     proof (simp add: r_congruent_def sym_def, clarify)
       fix x y