equal
deleted
inserted
replaced
127 |
127 |
128 |
128 |
129 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
129 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
130 by (simp add: permute_pure) |
130 by (simp add: permute_pure) |
131 |
131 |
132 (* TODO: should be provided by nominal *) |
|
133 lemmas [eqvt] = trm_assn.fv_bn_eqvt |
|
134 thm trm_assn.fv_bn_eqvt |
|
135 |
|
136 |
|
137 thm Abs_lst_fcb |
|
138 |
132 |
139 lemma Abs_lst_fcb2: |
133 lemma Abs_lst_fcb2: |
140 fixes as bs :: "'a :: fs" |
134 fixes as bs :: "'a :: fs" |
141 and x y :: "'b :: fs" |
135 and x y :: "'b :: fs" |
142 and c::"'c::fs" |
136 and c::"'c::fs" |