Introduce skolemization.
Recognise indexed variables and function symbols.
Update check_models().

Add support for constants, free variables and function symbols.
Test skolemization using check_models().