Mizar Aggregates

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

Hello,

The implementation of Mizar aggregates seems to be incomplete.
Namely, it is impossible (or I do not know how) to prove
that aggregates of two different structures are different.
For example, the sentence

 1-sorted (# NAT #) <>  ZeroStr (# NAT, 0 #)

is not acceptable, and, consequently, the sentence

 for S being strict 1-sorted, Z being strict ZeroStr holds S <> Z

is not.

It is not so important, but it may be convenient to have such
differences automatically. And it seems to be easy to implement.

Sincerely yours,
Grzegorz Bancerek