[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Record-type equality bug??



Hello,

I am having strange problems trying to prove a conjecture and I was wondering
if anybody could shed some light on it. The actual conjecture itself
does not appear to be important, but it ends up yielding sub-goals
of the following type:

headc3.2 :  

[-1]  (# un := 1, id := 1 #) = di!1
[-2]  (# un := 1, id := 0 #) = di!1
  |-------
[1]   (di!1`un = 0)

Shouldn't this be trivially proveable? Here, 'di!1' a variable of a normal
record type, defined as follows:
	UIndex: TYPE = [# un:nat, id:nat #]

Thanking you in advance,
Malcolm