| changeset 2082 | 0854af516f14 |
| parent 2057 | 232595afb82e |
| child 2104 | 2205b572bc9b |
| 2081:9e7cf0a996d3 | 2082:0854af516f14 |
|---|---|
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 declare alpha_gen_eqvt[eqvt] |
|
27 |
|
28 equivariance alpha_trm_raw |
|
29 |
|
30 |
|
25 end |
31 end |
26 |
32 |
27 |
33 |
28 |
34 |