Now let us look into the details of the Gallina language, in which we write terms and formulas. We have the l-calculus. Abstraction is denoted by square brackets, application is denoted in a trivial way, while universal quantification is denoted by the use of standard brackets. As usual, when x is not free in B the universal quantification can be seen as just a simple implication, and so it can be written as A®B.

---