The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Which book or other source are you reading to learn Coq?  Especially the 
first of these questions is pretty basic.

Victor Porton wrote:
> 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?
>   

Do (degenerate) "case analysis" on the constructor used to build each 
record, as [Record] is shorthand for [Inductive].

> 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)?
>   

The idea of a dependent record type has no fundamental concept of 
"conditions," so the question seems ill-formed.  You probably want to 
read about proof irrelevance.