src/HOL/BNF_Wellorder_Constructions.thy

   have "f12 ` ?A1 < ?A2"
   using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def)
   moreover have "inj_on f23 ?A2"
   using EMB23 0 by (simp add: wo_rel_def embed_inj_on)
   ultimately
-  have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: inj_on_strict_subset)
+  have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: image_strict_mono)
   moreover
   {have "embed r1 r3 (f23 \<circ> f12)"
    using 1 EMB23 0 by (auto simp add: comp_embed)
    hence "\<forall>a \<in> ?A1. f23(f12 a) = f13 a"
    using EMB13 0 embed_unique[of r1 r3 "f23 \<circ> f12" f13] by auto