equal
deleted
inserted
replaced
413 apply(simp add: supp_append) |
413 apply(simp add: supp_append) |
414 apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom) |
414 apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom) |
415 apply(rule conjI) |
415 apply(rule conjI) |
416 prefer 2 |
416 prefer 2 |
417 apply(auto)[1] |
417 apply(auto)[1] |
418 apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2)) |
418 apply (metis permute_atom_def_raw permute_minus_cancel(2)) |
419 defer |
419 defer |
420 apply(rule psubset_card_mono) |
420 apply(rule psubset_card_mono) |
421 apply(simp add: finite_supp) |
421 apply(simp add: finite_supp) |
422 apply(rule psubsetI) |
422 apply(rule psubsetI) |
423 defer |
423 defer |