 The possibility that \(e\) may contain free occurrences of variables (whose types are given by a basis \(B\)) slightly complicates the interpretation of terms, making it depend on a further parameter, an environment \(\rho\) mapping each free variable \(x:\tau\) of \(e\) to an element of \(D^\tau\) (if the latter condition is satisfied, we say that \(\rho\) respects \(B\)). Of course, the environment is irrelevant when \(e\) is closed.