Fixed soundness proofs to work with the new tactics of mirror-core.