The Coq mailing list

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

On 03/29/2012 04:58 PM, Bernard Hurley wrote:
> I am new to Coq and it seems to be an excellent piece of software, but I have
> come across something that doesn't seem to make sense.  If I do something 
> like:
> =================
> Inductive Atom: Set:= _A: nat ->  Atom.
>
> Lemma Test: forall A: Atom, exists m: nat, A = _A m.
> Proof.
>    induction A.
>    exists (x := n).
>    reflexivity.
> Qed.
> ===============
>
> The proof works OK.  However I would have expected to be able to use:
>
>    exists (m := n).
>
> But If I do I get the error message:
>
> Toplevel input, characters 14-29:
> Error: No such bound variable m.
>
> Why does this happen?  The variable 'm' looks bound to me!  And where did the
> 'x' come from?
>    

[x] comes from the definition of [ex], the type family to which uses of 
[exists] are expanded.  One command sequence to chase this down from 
first principles:
    Locate "exists".
    Print ex.