The Coq mailing list

[Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>]

Hello,

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.