Dear Yassmeen,
set comprehensions in HOL are a bit cryptic. They are explained in
Section 5.5.1.1 of the Description manual. In short, something like {t |
p} is syntactic sugar that is turned by the parser into GSPEC(\(x1
,...,xn). (t,p)). The trick is figuring out, which variables x1, ... xn
to
Hi,
I have this proof goal, where I need to prove that two sets are equal.
{{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
a |
a IN if j IN L then s3 j else s4 j} =
{{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
a IN if j IN L then s3 j
