equal
deleted
inserted
replaced
62 unfolding alphas |
62 unfolding alphas |
63 unfolding permute_eqvt[symmetric] |
63 unfolding permute_eqvt[symmetric] |
64 unfolding set_eqvt[symmetric] |
64 unfolding set_eqvt[symmetric] |
65 unfolding permute_fun_app_eq[symmetric] |
65 unfolding permute_fun_app_eq[symmetric] |
66 unfolding Diff_eqvt[symmetric] |
66 unfolding Diff_eqvt[symmetric] |
67 by (auto simp add: permute_bool_def fresh_star_permute_iff) |
67 unfolding eq_eqvt[symmetric] |
|
68 unfolding fresh_star_eqvt[symmetric] |
|
69 by (auto simp add: permute_bool_def) |
68 |
70 |
69 |
71 |
70 section {* Equivalence *} |
72 section {* Equivalence *} |
71 |
73 |
72 lemma alpha_refl: |
74 lemma alpha_refl: |