# The contraction of a given redex yields a unique result

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)

• I'm not sure to understand your question. If $(\lambda x.P)Q = (\lambda y. M)N$ ($=$ is always in the sense of $\alpha$-equivalence here), then $\lambda x.P = \lambda y.M$ and $Q = N$, from that it follows that $P[x:=Q] = M[y:=N]$ because substitution is compatible with $\alpha$-equivalence.. Commented May 9, 2023 at 9:32
• Ohh... it was that simple? Commented May 9, 2023 at 11:40

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..