In the popular FOL problem "Criminal West" of the Book AI Modern Approach, I'm unable to understand how it gets from step 3 to 4 in the proof tree as highlighted in this picture.
Image of proof tree of Criminal West problem
In the previous step I thought it like follows but I cannot get how Missile(y) replaces Weapon(y)
If American(West) is true then ¬American(West) becomes false and the remaining part should be true.
Missile(x) does not replace Weapon(x);
Here is how the process of unification of clauses works at this level:
$$\neg Missile(x) \lor \underbrace{Weapon(x) \ \ \ \ \ \ \ \ \neg Weapon(y)}_{\binom{\text{cancellable under the cond.}}{\text{that} \ x \ \text{is identified with} \ y.}} \lor \neg Sells(West,y,z) \lor \neg Hostile(z)$$
$$\text{Yielding the new clause:}$$
$$\neg Missile(y) \lor \neg Sells(West,y,z) \lor \neg Hostile(z)$$
The Weapons are "destroyed" in the process...
Remark: instead of keeping $y$, it could have been $x$...