TBox unfolding

Substitution of acyclic concept definitions into expressions to be tested. Primitive inclusions require care: $A⊑D$ can be represented using a fresh name $A_0$ by $A\equiv A_0\sqcap D$, but is not equivalent to $A\equiv D$.