src/HOL/UNITY/SubstAx.thy

 apply (rule_tac f = f and f1 = "%k. l - k" 
        in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
 apply (simp add: Image_singleton, clarify)
 apply (case_tac "m<l")
  apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
-apply (blast intro: not_leE subset_imp_LeadsTo)
+apply (blast intro: not_le_imp_less subset_imp_LeadsTo)
 done
 
 
 subsection{*Completion: Binary and General Finite versions*}