In this paper we deal with the extension of the functionalities of the TIL-Script language, namely the proof system based on natural deduction. The system processes a subset of the set of TIL-Script constructions that are typed to v-construct a truth-value. Since TIL-Script is a functional programming language based on a hyperintensional lambda calculus with procedural semantics, we also describe the way how to validly apply beta conversion and how to operate in a hyperintensional context where the very procedure is an object of predication.