equal
deleted
inserted
replaced
1 theory Nominal2_FSet |
1 theory Nominal2_FSet |
2 imports FSet Nominal2_Supp |
2 imports FSet Nominal2_Supp |
3 begin |
3 begin |
4 |
4 |
5 lemma permute_rsp_fset[quot_respect]: |
5 lemma permute_rsp_fset[quot_respect]: |
6 "(op = ===> op \<approx> ===> op \<approx>) permute permute" |
6 "(op = ===> list_eq ===> list_eq) permute permute" |
7 apply (simp add: eqvts[symmetric]) |
7 apply (simp add: eqvts[symmetric]) |
8 apply clarify |
8 apply clarify |
9 apply (subst permute_minus_cancel(1)[symmetric, of "xb"]) |
9 apply (subst permute_minus_cancel(1)[symmetric, of "xb"]) |
10 apply (subst mem_eqvt[symmetric]) |
10 apply (subst mem_eqvt[symmetric]) |
11 apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"]) |
11 apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"]) |