| changeset 2082 | 0854af516f14 |
| parent 2059 | c615095827e9 |
| 2081:9e7cf0a996d3 | 2082:0854af516f14 |
|---|---|
18 | App "trm" "trm" |
18 | App "trm" "trm" |
19 | Lam "ty" n::"name" t::"trm" bind_set n in t |
19 | Lam "ty" n::"name" t::"trm" bind_set n in t |
20 |
20 |
21 thm kind_ty_trm.supp |
21 thm kind_ty_trm.supp |
22 |
22 |
23 declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt] |
|
24 declare alpha_gen_eqvt[eqvt] |
|
25 |
|
26 equivariance alpha_trm_raw |
|
27 |
|
28 |
|
29 |
|
30 |
|
23 end |
31 end |
24 |
32 |
25 |
33 |
26 |
34 |
27 |
35 |