On Mon, Apr 21, 2008 at 10:51 AM, <dagreve@xxxxxxxxxxxxxxxxxxx> wrote: > > 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? Try (decompose-equality). -- Jerry James http://loganjerry.googlepages.com/