Re: If A=B & (A contains C), why mizar doesn't infer (B contains C)

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Josef Urban wrote:

> I think it is a good idea, to require that the checker would accept
> such inferences. There are some mechanisms in the checker that almost do
> this, e.g. if you first defined

> I think it would not be too difficult to implement this "forgetting of
> hidden arguments" in general case, not just for redefinitions.
>

You cannot just forget the hidden arguments. You may forget fictitious
arguments, it does not matter if they are hidden or visible. But if the
argument is ficitious, then why to have it among loci of the definition.

I believe it is important point: if we make the system even a bit more
complicated, it must be useful

Andrzej