[PVS-Help] cotuple proof

[dagreve@xxxxxxxxxxxxxxxxxxx]

I have defined a cotuple:

co: TYPE = [ int + bool ]

I would like to prove the following:

proof: LEMMA
  FORALL (x,y: int):
    IN_1(x) = IN_1(y) IMPLIES
(x = y) 

But I don't see how.  Is this possible?

  I looked at an equivalent DATATYPE
theory
and I don't  see how to do the
equivalent proof
there, either.

Thanks,
Dave