The Coq mailing list

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

Certainly the alternate proof that someone else suggested later is nicer 
than what I suggested, but mine didn't rely on any axioms. ;)

On 03/17/2013 08:36 AM, Thierry Martinez wrote:
> Leonardo:
>    
> > > Lemma unprovable :
> > >    forall q : H a, q = b.
> > >        
> Adam:
>    
> > Require Import Eqdep_dec.
> >      
> or without relying on an extra-CiC axiom:
>
> Proof.
> intro q.
> exact (match q with | b =>  eq_refl end).
> Qed.
>
> I don’t know how to ask tactics to build such a term