The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

> You can build a list of candidate hypotheses by getting each hypothesis out
> of the way as you first select it.  For instance, run [generalize dependent
> H] inside your loop, and then [intros] all the hypotheses back into place
> afterward, once you've built a list of hypotheses (say, as a tuple).

I don't understand how to build a list of hypotheses, but the
generalize dependent does the trick!

Thanks

- Alexandre Pilkiewicz