The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 09/12/2014 06:04 PM, Jonathan wrote:
> Inductive Erasable(A : Type) : Prop :=
>       erasable: A -> Erasable A.
>
>    Arguments erasable [A] _.
>
>    Axiom Erasable_inj : forall {A : Type}{a b : A}, erasable a=erasable
>    b -> a=b.

We did the same thing in Ynot, and I think this axiom turned out to be 
inconsistent, period.  You don't need to assume any others to run into 
trouble.  I don't remember the details of the proof, though.