Add spec form to cover both `INST` and `SPEC` of theorems

[mn200]

It should be possible to specialise variables without knowing where in a quantification block they are, and if free, the effect can be as of INST.