Email Gateway (Nov 10 2021 at 10:42): Email Gateway (Nov 10 2021 at 10:42):From: Emin Karayel <me@eminkarayel.de>
Hi Peter,
You can solve this using the OF attribute.
First proof (once):
lemma switch_eq:
assumes "(x=y) = z"
shows "(y=x) = z"
using assms by auto
Once you have that you can refer to the switched version of any lemma L of
the form [(x=y)=z] like this:
switch_eq[OF L]
For example:
switch_eq[OF filter_empty_conv] is the same as your empty_filter_conv
I hope this helps,
Emin
Last updated: Jan 04 2025 at 20:18 UTC