The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/12/2014 06:04 PM, Jonathan wrote:

Maybe there is a problem here?  I will try to create a contradiction in this case, using a Prop that is identical in structure to Erasable, but just not itself Erasable - that actually does look possible...

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.

Inductive Foo(A : Type) : Prop :=
  foo: A -> Foo A.
 
Arguments foo [A] _.

Set Injection On Proofs. (*fails with or without this*)

Goal forall i j:nat, foo i=foo j ->erasable i=erasable j.
intros i j H.
Fail injection H.

I can't find a proof for that - can anyone else?

-- Jonathan