The Coq mailing list

[George Van Treeck <treeck AT yahoo.com>]

I have a "Variable A : Type." and a lemma that uses "forall (a: A) (l: list A),...". When I apply that lemma it to another lemma, which only uses "forall (l: list A),...", then Coq leaves a final goal of "A" that I can't clear.

I can work around this problem by adding the variable, "(a:A)", to use assumption to clear the "A" goal. But, it's an ugly hack because the variable, a, isn't actually used in the lemma. Is there a more elegant way to clear the goal "A"? I'm using Coq versioin 8.4p16.

-George