[STATEMENT]
lemma find_remove_2_removeAll :
  assumes "find_remove_2 P xs ys = Some (x,y,xs')"
  and     "distinct xs"
shows "xs' = removeAll x xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs' = removeAll x xs
[PROOF STEP]
using find_remove_2_set(6)[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
xs' = remove1 x xs

goal (1 subgoal):
 1. xs' = removeAll x xs
[PROOF STEP]
by (simp add: assms(2) distinct_remove1_removeAll)