[ refactor ] Added strengthening constructor to substitution type

Previously we were substituting with __IMPOSSIBLE__ terms all over
the place, when we were sure that the corresponding variable was
unused. This is problematic if you want to optimise substitution
(for instance, simplify Var 0 [] :# Wk 1 IdS to IdS), since you
can't look at the term. To fix this you should now use

  new: Strengthen __IMPOSSIBLE__ rho
  old: __IMPOSSIBLE__ :# rho

  new: strengthen __IMPOSSIBLE__ v
  old: subst v __IMPOSSIBLE__

  new: compactS __IMPOSSIBLE__ [Just u, Nothing, Just v]
  old: parallelS [u, __IMPOSSIBLE__, v]

  new: noabsApp __IMPOSSIBLE__ u
  old: absApp u __IMPOSSIBLE__

To help catch incorrect uses of subst and friends, the
substitution building functions are now strict in the term. The
exception is 'lazyAbsApp' which is used in 'apply', which still
allows __IMPOSSIBLE__ terms. It'd be nice to get rid of that too
but I didn't want to change the type of 'apply'.
[ issue1303 ] updated unquote error message