| changeset 2093 | 751d1349329b |
| parent 2082 | 0854af516f14 |
| child 2104 | 2205b572bc9b |
| 2092:c0ab7451b20d | 2093:751d1349329b |
|---|---|
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 declare alpha_gen_eqvt[eqvt] |
|
32 |
|
33 equivariance alpha_trm_raw |
|
34 |
|
35 |
|
30 end |
36 end |
31 |
37 |
32 |
38 |
33 |
39 |