Fix injectivity checking, again (#17405)

We were previously doing injectivity checks on all type family instances in scope, even those imported (and presumably checked) in another module. Now, we just check imported equations for conflicts. And there is some refactoring; see commit message.

I've kept this as two commits, because they're actually separate. But if Marge dislikes this, I'll squash.