WYCS: making some kind of progress
WYCS: simplified the syntax for quantifiers to remove the very awkward distinction between bounded and unbounded variables.