It now copies the hypothesis when: 1.) it is persistent 2.) when destructing
it requires a universal quantifier to be instantiated. The new behavior is
implemented using a type class (called CopyDestruct) so that it can easily be
extended.