Re: [mizar] Isn't "Subset of" the same as "Element of bool"?

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Grzegorz,

Thanks for your quick and thorough explanation.  But...

>Expandable definitions are "static", i.e., any redefinition
>of constructors which are given after "is" has no impact on
>identification.

That's surprising to me!

>They are stored in terms of constructors and no any
>connection with notation is recognized.

But surely there's some kind of automatic equality between
the old and the new constructors? I mean, the theorems for
the "old" bool still apply to the "new" bool, don't they?  So
why doesn't the typing work like that?

>It is better to repeat expandable definition after
>redefinition of "bool".

Okay, if that's a solution then I'll use it (although you'll
have to admit that it looks silly).  However, I fear I won't
be able to explain what goes wrong in this example to others.

Freek