The ex subdirectory contains some examples.
NB: the formalization is not completely sound! It does not enforce distinctness of variable names in contexts!
For more information about the Lambda-Cube, see