subsection ‹Ground constructions› theory Ground_Terms imports Basic_Utils begin subsubsection ‹Ground terms› text ‹This type serves two purposes. First of all, the encoding definitions and proofs are not littered by cases for variables. Secondly, we can consider tree domains (usually sets of positions), which become a special case of ground terms. This enables the construction of a term from a tree domain and a function from positions to symbols.›