The Coq mailing list

[Victor Porton <porton AT narod.ru>]

From the following it seems that it is totally impossible to compare 
dependent records.

Error: The term "@v B" has type "@x B = 0" while it is expected to have type
 "@x A = 0".

Are there any idea how to circumvent this problem?

[[[
Class C := {
  x : nat;
  v : (x=0)
}.

Parameter A B : C.

Axiom ax: @x A = @x B.

(* Now I'll attempt to prove [A = B]. *)
(* But my proof doesn't work with a confusing error message:
Error: The term "v" has type "x = 0" while it is expected to have type
 "x = 0".
*)

Set Printing Implicit.

Theorem ax2: @v A = @v B.
Proof.
  auto.
Qed.

Theorem thm: A = B.
proof.
  thus thesis by ax, ax2 using injection.
end proof. Qed.
]]]

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