| changeset 2105 | e25b0fff0dd2 |
| parent 2104 | 2205b572bc9b |
| child 2120 | 2786ff1df475 |
| 2104:2205b572bc9b | 2105:e25b0fff0dd2 |
|---|---|
25 thm trm_pat.perm |
25 thm trm_pat.perm |
26 thm trm_pat.induct |
26 thm trm_pat.induct |
27 thm trm_pat.distinct |
27 thm trm_pat.distinct |
28 thm trm_pat.fv[simplified trm_pat.supp(1-2)] |
28 thm trm_pat.fv[simplified trm_pat.supp(1-2)] |
29 |
29 |
30 declare permute_trm_raw_permute_pat_raw.simps[eqvt] |
|
31 |
|
32 equivariance alpha_trm_raw |
30 equivariance alpha_trm_raw |
33 |
31 |
34 |
32 |
35 end |
33 end |
36 |
34 |