Add background theory and type axioms for skolem constants.
Remove T(T(x)) = T(x) axiom as we now add axioms for skolem variables.