minor changes to unif and type inference
commented tools/detect_theories code until everything is ready;
updated signatures of meta-prover after more thought
partial implementation of the meta-prover (reasoner not finished)