TESTS: added another test case
WYCS: minor tweak to quantifier instantiation