The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

It is indeed provable if you suppose decidability of equality on C. I
don't know if there is a weaker suitable supposition.

Of course there is: namely the asserion that [c=c'] is negative. Now, this is quite beyond the stage of nitpicking. But it's fairly generic too: classical reasoning is valid on negative formulæ. For weaker principle may be possible to force them without going full negative (though I'm not the right person to ask how). But here, we need full-blown double negation elimination, so this is, I assume, optimal.

Variable C N: Set.
Variable F: C-> N.
Axiom A: forall c c': C, (~ (c = c')) <-> (~ (F c = F c')).
Axiom Ceqneg: forall c c':C, ~~ c=c' -> c=c'.

Theorem T: forall (n: N) (c: C), F c = n -> forall c': C, F c' = n -> c = c'.
Proof.
  intros * <- * h.
  apply Ceqneg. intros hc.
  apply -> A.
  + exact hc.
  + symmetry. exact h.
Qed.