bugfix in formula;
apply substs to formulas;
alpha-equivalence checking for formulas
Skolem and Cnf now back in Logtk.base