thread along context instead of theory for typedef lookup

obsolete FIXME

move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it; "size_change" rarely needs anything beyond "dpll", so this warning is annoying at best, and when "size_change" is called from Nitpick the warning confuses users, who then think that Nitpick is using "dpll" when it's really using MiniSat or some other fast solver

don't include any axioms for "TYPE" in Nitpick

dropped obsolete script

normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);