Gödel’s System \(\T\) is essentially intuitionistic type theory with only the type formers \(\N\) and \(A \rightarrow B\) (the type of functions from \(A\) to \(B\), which is the special case of  \((\Pi x {:} A)B\) where \(B\) does not depend on \(x {:} A\)). Since there are no dependent types in System \(\T\) the rules can be simplified.