equal
deleted
inserted
replaced
61 | "\<lbrakk>\<exists>pi.({atom name} \<union> {atom coname1}, trm_raw) \<approx>gen alpha fv_trm_raw pi |
61 | "\<lbrakk>\<exists>pi.({atom name} \<union> {atom coname1}, trm_raw) \<approx>gen alpha fv_trm_raw pi |
62 ({atom namea} \<union> {atom coname1a}, trm_rawa); coname2 = coname2a\<rbrakk> \<Longrightarrow> |
62 ({atom namea} \<union> {atom coname1a}, trm_rawa); coname2 = coname2a\<rbrakk> \<Longrightarrow> |
63 alpha (ImpR_raw coname1 name trm_raw coname2) |
63 alpha (ImpR_raw coname1 name trm_raw coname2) |
64 (ImpR_raw coname1a namea trm_rawa coname2a)" |
64 (ImpR_raw coname1a namea trm_rawa coname2a)" |
65 |
65 |
|
66 thm alpha.intros |
|
67 |
|
68 declare permute_trm_raw.simps[eqvt] |
|
69 declare alpha_gen_eqvt[eqvt] |
|
70 |
|
71 equivariance alpha |
|
72 thm eqvts_raw |
|
73 |
66 |
74 |
67 end |
75 end |
68 |
76 |
69 |
77 |
70 |
78 |