Hi,
On Mon, 21 May 2007, Jesse Alama wrote:
I can get the second case to go through, but the first case, where A is
assumed to be empty, gives me trouble: I can't finish the proof that X
is empty.
I then gave up on (*) and moved to
X := (***) { x where x is Element of A : <whatever> & x in A }
With this change my proofs go through, but (***) seems ham-handed to me.
My question for the experts: what other ways are there of dealing with
the problem besides (***)?
To me it's the only solution in this case, albeit an ugly one.
Why was I unable to get the desired typing judgment with (*)?
According to the current MML definition of 'Element of', it's simply not true
(in the case X={} ) that
X = {x: where x in Element of X: not contradiction}
because {} is not equal to {{}}. And for the same reason { x where x is
Element of A : <whatever>} needn't be a subset of A