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

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

Piotr Rudnicki wrote:

> On Mon, Jun 25, 2001 at 07:53:14PM +0200, Andrzej Trybulec wrote:
>
> How to get rid of that *84 error?

I apologize. I see that what I wrote was misleading.

I a hot version Grzegorz found an error (we did not check if the Result Type is
invariant wrt switching the arguments). It is corrected now. So you cannot get rid
of *84 error (fortunately).

Andrzej