2309     case (plus p1 p2)

  2309     case (plus p1 p2)

  2310     have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+

  2310     have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+

  2311     then show "(p1 + p2) \<bullet> x = x" by simp

  2311     then show "(p1 + p2) \<bullet> x = x" by simp

  2312   qed

  2312   qed

  2313 qed

  2313 qed

  2314 

  2317 

  2315 lemma supp_perm_perm_eq:

  2318 lemma supp_perm_perm_eq:

  2316   assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"

  2319   assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"

  2317   shows "p \<bullet> x = q \<bullet> x"

  2320   shows "p \<bullet> x = q \<bullet> x"

  2318 proof -

  2321 proof -