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

records



Hi,

How can I prove a goal like this:

[-1]    (# b := TRUE,
         p := (# n := top!1, h := (# f := FUn!1, s := Sn!1 #) #),
         v := 0 #)
          = rec!1 WITH [p := prod!1 WITH [n := i!1]]
  |-------
[1]    i!1 = top!1


Assert, grind do not help, though it seems that all it has to do is
to identify the two n fields.


Thanks,
Monica Marcus