The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

Hi,

I have a goal with "forall c : C, ... " in the assumptions, for
which apply fails for various reasons. I was not able to
instantiate it and finally solved the problem with cut. IMO this
use of cut is a bad workaround, because it requires to copy the
complete body of the forall and to perform the substitution
manually. 

How can I manually instantiate a universal
quantification/dependent product in the assumptions?

Bye,

Hendrik