Are these advanced theorem proving benefits obtainable with static typing alone, or does everything also have to be effect free ("purely funtional")?
You can apply the same intuition and things mostly work, but there can be a few surprises.
These theorems are a huge part of the "if it compiles it must be correct" feeling that functional programming often provides.