WYCS: working on putting bounded quantifiers back.