I think this is all that's needed, right? I've already used this statement (with the iProp-only proof) to simplify the ugly proofs @robbertkrebbers saw today — and this adds no obligation on the interface.