Implement `Control.Function.Injective` for `Data.SOP.NS.Z`, `Data.SOP.NS.S`, `MkPOP`, `Data.SOP.NP.(::)`, and `MkSOP`?

[jmanuel1]

This is really a feature request... but there are already private proofs of injectivity for these constructors.