The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Record T := {
  x y : num
}.

Variable A B : T.

Now suppose we know [x A = x B] and [y A = y B]. Which ways we may infer [A = 
B] from that?

Also what about dependent records? Are they equal even in the case if they 
have different justifications (proved by different lemmas)? Can we infer 
equality of two dependent records comparing only data fields (not the 
conditions)?

What is the idea behind comparing dependent records?

-- 
Victor Porton - http://portonvictor.org