However, a type proof can show that reverse, reverses all possible strings.

It is possible to test that a function on 16 bit integers returns the correct value for all inputs. Doing so would be a proof by exhaustion.

Type based proofs let us prove things using other methods than exhaustion, which is the only possible way to prove things with tests. That is an important property.