Support explicit naming of hypotheses generated by funelim

[anton-trunov]

It would be great to have a variant of funelim like induction foo as [... | ... | ...] or better yet for compatibility with the Mathcomp style an option to not move everything into the context.

[mattam82]

There is the apply_funelim tactic which does not introduce hypotheses.

[Tuplanolla]

The apply_funelim tactic should be mentioned in the reference manual.