The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

In the Qcanon library, last theorem is:

Theorem Qc_decomp: forall x y: Qc,
  (Qred x = x -> Qred y = y -> (x:Q) = y)-> x = y.

This is right of course, but I do not see the point in having
"Qred x = x -> Qred y = y -> (x:Q) = y"

Why not simply
"(x:Q) = y"

provided that "Qred x = x" is always true
(a proof is given by "canon x") and same thing applies for "Qred y = y"

If it were a lemma, I would understand, but stating it as a theorem is
really strange for me.