The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Pierre-Marie Pédrot wrote:
> I am currently facing a somewhat simple problem which is very close to
> one example that can be found in Adam's book :
>
> Lemma tricky : forall (A : Type) (X : A) (pf : A = A), X = match pf in
> (_ = A) return A with refl_equal =>  X end.
>
> [...]
>
> Any clues (axiom-free, of course) ?
>    

It seems likely that you can't prove this without an axiom.  Note that 
your theorem is _very_ close to the [Eqdep] module's axiom:
    http://coq.inria.fr/stdlib/Coq.Logic.Eqdep.html
If you unfold the definition of [eq_rect] there, the statement is almost 
your [tricky] lemma.  The only generalization is allowing any [return] 
clause, not just [return A].

Whoever thought hard about metatheory here concluded that [eq_rect_eq] 
isn't provable.  Maybe your specialization of it _is_ provable, but I'm 
not aware of a proof.