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.