This change makes it possible to use hlists in the proof mode, which
itself uses hlists in the implementation of the specialize tactic.