The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Hi,

I get the following errors:

gen_moveL < apply midI3.
Toplevel input, characters 6-11:
 > apply midI3.
 >       ^^^^^
Error: The reference midI3 was not found in the current environment.

gen_moveL < Check midI3.
Toplevel input, characters 6-11:
 > Check midI3.
 >       ^^^^^
Error: The reference midI3 was not found in the current environment.

gen_moveL < Lemma midI3: forall T (a b c d : list T) (x y : T),
   a = c -> b = d -> a ++ x :: b = c ++ x :: d.
gen_moveL < Toplevel input, characters 6-11:
 > Lemma midI3: forall T (a b c d : list T) (x y : T),
 >       ^^^^^
Error: midI3 already exists.

I'm in the middle of a long proof, in which I have previously proved a 
useful lemma, called midI3.

Presumably the lemma I've proved is considered (though not actually) to 
depend somehow on the particular state of the proof at which I first 
proved it.  Would that be right?

but it seems the system won't let me use it at the current point in my 
proof, and won't let me prove it again.

So my question is, having decided during a proof that a particular lemma 
would be useful, how to I prove and use it?

thanks

Jeremy