WYCS: various minor improvements.  It remains to handle quantifier instantiation properly though.