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.