Generalize (e)feed pose proof to intro patterns

This appears a simple oversight, since pose proof takes an intro pattern anyway; feed inversion and feed destruct already take intro patterns, and I've been using the generalized efeed pose proof for a while.

More intro patterns is better.

However, I'd like to understand the rationale: what is the advantage compared to using destruct and edestruct here? They already create goals for all arguments.

ping @Blaisorblade

closed

I'll recheck, but I suspect the advantage is indeed not there, and I have already replaced some uses of this tactic back with destruct; I think I didn't realize at first. An brief comment suggesting (e)destruct might be appropriate, but maybe not worth it.