Another thing I noticed about drule* and I believe irule as well is that
they treat free variables as universally quantified so they don't conserve
prior specialization. The idiom I found to work around it is to qspecl_then
[list of specialization] mp_tac thm to get new goal as thm ==> old goal,
I think I really like how drule and drule_all work, but is there something
that walks the middle road? I mean drule only discharges one condition; and
drule_all needs all conditions to be discharged. It would be nice to have a
drule that discharges as many as possible and leave the rest as
