The Coq mailing list

[Victor Porton <porton AT narod.ru>]

[[[
Definition A := { x:nat | x > 1 }.

Record B := {
             x: nat;
             c: x > 1
}.
]]]

A and B are essentially the same thing.

But for proofs of equality of objects of type B proof irrelevance is 
required, while for proofs of equality of objects of type A proof irrelevance 
is not required. Right?

What is the deep reason of proof irrelevance required in one case and not 
required in an other case?

It seems I misunderstand something.

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