The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/12/2014 06:10 PM, Adam Chlipala wrote:
> 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.

Wow - really?  Does anyone remember those details?

-- Jonathan