Lets say we were trying to determine whether the following equation is satisfiable, and we decide to compute the most general common unifier:

f x w = f (g y) z

To solve it, we must have injectivity. The rule allows us to move into the next step:

x = (g y) ∧ (f` w) = (f` z)

The (f’) in the expression is the ‘f’ function with one parameter filled in.
Now we can further move on.

x = (g y) ∧ w = z

Now we have equations that have a variable on another side of a term. We have found the most general common unifier. Ok, Injectivity is required so you can do this.

Type families are arbitrary equations mapping types to other types. I don’t remember the exact syntax, but something like:

type family F a where
F Int = String
F String = String
F a = a

If you assumed injectivity, you could prove that Int ~ String. I think GHC supports injective type families, which are essentially functional dependencies on the type family.