A Universe of Sorts

To decide some kind of property involving free variables, we split it into two parts:
First, closed term that interns all free variables into an AST (makes them into bvars), so we have e.g. decidable equality on it, which is closed.
An environment that refers to the local context (i.e. the fvars), which needs to be built by metaprogramming.
So, for example, to implement something like ring, we have a part that uses bvars to be able to build closed terms, and a decidable "isomorphism" predicate which shows that they will be equal.

§ Boolean Reflection Design