The Coq mailing list

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

Yes, it's provable.  For an explanation of what's going on in this 
proof, and also of the problems you probably ran into originally, I 
recommend Chapter 10 of CPDT <http://adam.chlipala.net/cpdt/>.

Require Import Eqdep_dec.

Lemma T_dec : forall x y : T, {x = y} + {x <> y}.
  decide equality.
Qed.

Lemma unprovable' :
  forall x (q : H x) Heq, q = match Heq in _ = T return H T with 
eq_refl => b end.
Proof.
  destruct q.
  intros.
  rewrite (UIP_dec T_dec Heq eq_refl).
  reflexivity.
Qed.

Lemma unprovable :
  forall q : H a, q = b.
Proof.
  intros; rewrite (unprovable' a q eq_refl); reflexivity.
Qed.


On 03/16/2013 08:31 PM, Leonardo Rodriguez wrote:
> Consider the following types:
>
> Inductive T : Type :=
>   a : T.
>
> Inductive H : T -> Type :=
>   b : H a.
>
> I have proved this trivial lemma:
>
> Lemma provable :
>   forall x : T, x = a.
> Proof.
>   intro x.
>   destruct x.
>   auto.
> Qed.
>
> But I couldn't prove this one:
>
> Lemma unprovable :
>   forall q : H a, q = b.
> Proof.
>   intro q.
> Abort.
>
> Could anyone explain me why? Has to do with proof irrelevance?
>
> Thank you in advance.