# Why is Church-Rosser so important for basing programming languages on lamdba-calculus?

So, I know Church-Rosser has 2 thesis:

CR1: If $E_1 \leftrightarrow E_2$, then there exists an Expression E so $E_1 \rightarrow E$ and $E_2 \rightarrow E$

CR2: If $E \rightarrow N$ (with N in normalform), then there exists a reduction row in normalorder (first reduce the left most ouuter most index) from E to N

from CR1 we learn that no expression can be converted to 2 different normalforms, so there is only one result for each function

from CR2 we learn that reduction in normalorder always finds the result (if their is one (no loop))

But i don't understand why these two are so important for basing a programming language on lambda-calculus. So my question is why are they?

Imagine that CR didn't hold, and that the order you evaluated an expression mattered. We would throw Lambda calculus away. It would be like saying $2+2$ could have more than one value.