1656 lemma swap_set_not_in_at:

  1656 lemma swap_set_not_in_at:

  1657   fixes a b::"'a::at"

  1657   fixes a b::"'a::at"

  1658   and   S::"'a::at set"

  1658   and   S::"'a::at set"

  1659   assumes a: "a \<notin> S" "b \<notin> S"

  1659   assumes a: "a \<notin> S" "b \<notin> S"

  1660   shows "(a \<leftrightarrow> b) \<bullet> S = S"

  1660   shows "(a \<leftrightarrow> b) \<bullet> S = S"

  1662   using a by (auto simp add: permute_flip_at)

  1662   using a by (auto simp add: permute_flip_at)

  1663 

  1663 

  1664 lemma removeAll_eqvt[eqvt]:

  1664 lemma removeAll_eqvt[eqvt]:

  1665   shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"

  1665   shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"

  1666 by (induct xs) (auto)

  1666 by (induct xs) (auto)