WYCS: disabled bounded quantifiers after all that; going to try and do it with quantification explicitly.
WYCS: fix for bounded quantification
WYCS: making slow progress ...