| changeset 2105 | e25b0fff0dd2 |
| parent 2104 | 2205b572bc9b |
| child 2120 | 2786ff1df475 |
| 2104:2205b572bc9b | 2105:e25b0fff0dd2 |
|---|---|
20 |
20 |
21 thm trm_lts.eq_iff |
21 thm trm_lts.eq_iff |
22 thm trm_lts.induct |
22 thm trm_lts.induct |
23 thm trm_lts.fv[simplified trm_lts.supp] |
23 thm trm_lts.fv[simplified trm_lts.supp] |
24 |
24 |
25 declare permute_trm_raw_permute_lts_raw.simps[eqvt] |
|
26 |
|
27 equivariance alpha_trm_raw |
25 equivariance alpha_trm_raw |
28 |
26 |
29 |
27 |
30 end |
28 end |
31 |
29 |