The Coq mailing list

[Victor Porton <porton AT narod.ru>]

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

Parameter set : Set.

Parameter A B : C set.

Axiom ax: @x set A = @x set 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".
What is the error?
*)

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

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

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