@natecull @akkartik @seanl

The Curry-Howard correspondence is between Simpled Typed Lambda Calculus and Propositional Intuisionistic Logic.

Per Martin-Löf added dependent types, types that can depend on the value of their arguments, to create Intuisionistic Type Theory which corresponds to Intuisionistic Predicate Calculus.

So with that bigger TT, you can prove stuff on computers like:

https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Nat.idr#L480