How about we pursue the SegWit softfork, and at the same time* work on a
hardfork which will simplify the proofs and reduce the kludgeyness of merge-
mining in general? Then, if the hardfork is ready before the softfork, they
can both go together, but if not, we aren't stuck delaying the improvements of
SegWit until the hardfork is completed.