No, not really. Under Curry-Howard, if you have a total function that returns an integer, you’ve proven that an integer exists. But we knew that already.

To prove non-trivial things, you need more sophisticated types that make interesting assertions about their values, where it’s not immediately obvious how to construct a value of that type. Special proof languages are used for this.