src/HOL/IMP/Abs_Int0_fun.thy

   assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'"
   have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
   have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     by(simp add: strip_lpfpc[OF _ 1])
   have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
-  proof(rule lfp_lowerbound[OF 3])
+  proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
       show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
       show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2])
     qed