The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jason, Jonathan,

thanks for the solution and explanation.

I experimented a bit. I think that this works for any literal term of any 
type, even if it doesn't have decidable equality. E.g.:

Open Scope list_scope.

Lemma TestNatList: forall (T : Type) (feq : 3::nil=3::nil->T) (H1 : 
3::nil=3::nil), feq eq_refl = feq H1.
Proof.
  intros.
  refine (match H1 with
          | eq_refl _ => _ 
          end).
  reflexivity.
Qed.

The resulting proof term is lengthy. I guess the decidable equality is 
required if the value compared is not a literal, but a parameter.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928