The Coq mailing list

[Bernard Hurley<bernard AT marcade.biz>]

Hi all,

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?

Thanks,

Bernard.