Gen_proofmode: move internal eq into SBI

If the Bi is not step-indexed, then there is no reason not to use the pure embedding.