The Coq mailing list

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

On 12/24/2011 02:28 PM, Marko Malikoviæ wrote:
> The second solution does not fit to me because if I put "foo" instead of
> all occurences of a = b then I can have foo and ~foo in the same
> hypothesis.
>    

Glad to hear that Chung-Kil's suggestion works.  I don't see the problem 
with using a named context, because such a context only has a single 
hole to be filled, even if the term initially found in that position 
appears multiple times in the goal.  Filling the hole will only put 
[foo] in that single position.