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

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

> in the Chen's example; in his example is something more
> complicated: locus becomes inaccessible, after widening the type of another
> locus. If the locus does not occur either in definiens or in the type
> involved, then it may be removed without any problem. 

If I understand this correctly, I think there still may be a problem,
incase there is a conditional or functor cluster defined for the more
special type (the type before widening).

Josef