| changeset 2105 | e25b0fff0dd2 |
| parent 2104 | 2205b572bc9b |
| child 2120 | 2786ff1df475 |
| 2104:2205b572bc9b | 2105:e25b0fff0dd2 |
|---|---|
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 |
|
25 equivariance alpha_trm_raw |
23 equivariance alpha_trm_raw |
26 |
24 |
27 |
25 |
28 |
26 |
29 |
27 |