Variants of depind/depelim that leaves hypothesis on the goal

[kyoDralliam]

This PR tries to provide a variant dep_elim of depind that leaves all the non-simplified hypothesis in the goal.

It uses elim instead of induction (but that might not be a useful change since we anyway mark the context and revert everything before it in the simplification phase).

TODO:

• [ ] maybe find a less conflicting name than dep_elim
• [x] implement the tactic for HoTT and Type (and not only for Prop)
• [x] provide a similar tactic for depelim