The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Sep 12, 2014 at 3:17 PM, Jonathan 
<jonikelee AT gmail.com>
 wrote:
> 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?

Goal forall {A:Type} (x y:A), foo x = foo y ->
  erasable x = erasable y.
Proof.
set (foo_impl_erasable := fun (A:Type) (H:Foo A) =>
   match H return (Erasable A) with
   | foo a => erasable a
   end).
intros.
apply f_equal with (f := foo_impl_erasable A) in H.
simpl in H.
assumption.
Qed.
-- 
Daniel Schepler