more thorough strip_shyps for proof boxes (but types are usually stripped and reconstructed later);