| changeset 2104 | 2205b572bc9b |
| parent 2082 | 0854af516f14 |
| child 2105 | e25b0fff0dd2 |
| 2103:e08e3c29dbc0 | 2104:2205b572bc9b |
|---|---|
27 |
27 |
28 thm exp_lrb_lrbs.eq_iff |
28 thm exp_lrb_lrbs.eq_iff |
29 thm exp_lrb_lrbs.supp |
29 thm exp_lrb_lrbs.supp |
30 |
30 |
31 declare permute_exp_raw_permute_lrb_raw_permute_lrbs_raw.simps[eqvt] |
31 declare permute_exp_raw_permute_lrb_raw_permute_lrbs_raw.simps[eqvt] |
32 declare alpha_gen_eqvt[eqvt] |
|
33 |
32 |
34 equivariance alpha_exp_raw |
33 equivariance alpha_exp_raw |
35 |
34 |
36 end |
35 end |
37 |
36 |