Email Gateway (Aug 18 2022 at 10:42): Email Gateway (Aug 18 2022 at 10:42):From: Cristiano Longo <cristiano.longo@tvblob.com>
I can prove the following lemma
"x \<in> {} = x mem []"
but, simplyfing this one
"x mem [] = x \<in> {}"
it results as False.
thanks in advance,
Cristiano Longo
Email Gateway (Aug 18 2022 at 10:43):From: Amine Chaieb <chaieb@in.tum.de>
This is the same behaviour as your last email. If you want the goal to
be parsed as an If and only if, the bracket it, otherwise use the <-->
symbol, it is = on bool with the usual prioities.
Of course x mem x is not a member of the empty set.
Amine.
Cristiano Longo wrote:
Last updated: May 03 2024 at 04:19 UTC