[jroesch]

If you have a system that allows you to write down the semantics of these expressions you can easily prove equivalence. You can use many of the techniques posted by others to construct such a proof for example functional extensionality is one method.

This is why dependent type theory is useful for reasoning about program behavior and program equivalence. For example it becomes possible show that a compiler is semantics preserving by demonstrating that the input and output program are "equivalent" in this way.

One issue with blindly translating a subset of expressions to SMT is that you may give them behavior different then the original source program. SMT solvers like Z3 have a builtin semantics for the logic, which may or may not reflect the source program you wrote. Verification languages that use SMT solvers for automated reasoning must be very careful about how they "compile" the source code into SMT queries to ensure that the query actually corresponds to the original program.