src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy

 lemma semiconfluentp_cancel1: "semiconfluentp cancel1\<inverse>\<inverse>"
   by(auto simp add: semiconfluentp_def rtranclp_conversep dest: cancel1_semiconfluent)
 
 lemma retract_cancel1_aux:
   assumes "cancel1 ys (map f xs)"
-  shows "\<exists>zs. cancel1 zs xs \<and> ys = map f zs"
+  shows "\<exists>zs. cancel1 zs xs \<and> ys = map f zs \<and> set zs \<subseteq> set xs"
   using assms
   by cases(fastforce simp add: map_eq_append_conv append_eq_map_conv intro: cancel1.intros)
 
 lemma retract_cancel1:
   assumes "cancel1 ys (map f xs)"
-  shows "\<exists>zs. eq xs zs \<and> ys = map f zs"
+  shows "\<exists>zs. eq xs zs \<and> ys = map f zs \<and> set zs \<subseteq> set xs"
   using retract_cancel1_aux[OF assms] by(blast intro: symclpI)
 
 lemma cancel1_set_eq:
   assumes "cancel1 ys xs"
   shows "set ys = set xs"