I want to prove that if $$(\lambda x. P)Q=(\lambda y. M)N$$ then $$P[x:=Q]= M[y:=N]$$ which means that the contraction of a given redex yields a unique result (so we don't have beta equivalence, but alpha equivalence).
I would go for a proof by contradiction but I think it should be prooved by a variation of structural induction, as it seems quite a hasty conclusion that an occurence of x (or y) hasn't been substituted and that's why contractum's differ.
Though I have neither seen any variation of induction used somewhere, nor I can use it without proof.
So could anyone help?
I am studying from "Lectures on the Curry"-Howard isomorphism-Sorensen, Urzyczyn (2006)
Transferring here the answer in the comments so that the question won't be left in the unanswered posts forever.
I'm not sure to understand your question. If $(.)=(.)$ (= is always in the sense of $$-equivalence here), then $.=.$ and $=$, from that it follows that $[:=]=[:=]$ because substitution is compatible with $$-equivalence..