Bugfixes: missing quantifier in `ExLam` constraint; freshening of existential type scheme; use whole premise in determining which disjunct is correct. More logging.