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

["Chen, Jing Chao (Jing Chao)" <jchen33@lucent.com>]

Sorry,I misunderstood Piotr's meaning, please ignore 
the previous message.

Piotr Rudnicki wrote

> The way you have defined predicate 'contains' (strange name 
> for what you
> write in the definiens) it has three arguments and from the fact that
> two of them are equal we cannnot infer what you want as with a 
> different definiens it may be not true.

  if it may be not true, could you give me such an example ? So
 far, I cannot find such an example.
  
J.C. Chen

> (Jing Chao) wrote:
> > Recently, I found that the proof of a very simple 
> proposition cannot be
> > accpted by Mizar.
> > For example
> > definition
> >  let f, tm be set, t be Subset of tm;
> >  pred t contains f means
> >       t c= f;
> > end;
> > 
> >  for f, tm1 be set, t1 be Subset of tm1,
> >  tm2 be set, t2 be Subset of tm2 st
> >     t1 contains f & t1=t2 holds t2 contains f;
> > ::>                 *4
> > This proposition can be simplified into 
> >    A=B & (A contains C)  => B contains C.
> > Clearly, it is ture. However, Mizar presented error 4.
> > What deduction mechanism doesn't allow such an inference ?
> > 
> > Jingchao Chen