equal
deleted
inserted
replaced
568 lemma [eqvt]: |
568 lemma [eqvt]: |
569 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
569 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
570 unfolding prod_fv.simps |
570 unfolding prod_fv.simps |
571 by (perm_simp) (rule refl) |
571 by (perm_simp) (rule refl) |
572 |
572 |
|
573 lemma prod_fv_supp: |
|
574 shows "prod_fv supp supp = supp" |
|
575 by (rule ext) |
|
576 (auto simp add: prod_fv.simps supp_Pair) |
|
577 |
|
578 lemma prod_alpha_eq: |
|
579 shows "prod_alpha (op=) (op=) = (op=)" |
|
580 unfolding prod_alpha_def |
|
581 by (auto intro!: ext) |
|
582 |
573 |
583 |
574 end |
584 end |
575 |
585 |