An important property of this isomorphism is that it is preserved under normalisation. Suppose we have a derivation where a redex is introduced. We know by the beta-rule computation that this term reduces to another term, that is to M where N is substituted for x. Now, the contraction which makes sense at a computational level makes deep sense also at a logical level. It is simply what in natural deduction is called the normalisation of proofs, a notion studied by Prawitz in the '60s and which once again corresponds exactly to the beta-rule of functional languages.

---