Change while case for "out" to only invariant.

flow_subset theorem for original out definition is not provable for following
program

ACQ wl ;;
WHILE b DO
	REL wl
END

[TODO] Current out is partial function and is not defined when "c" changes the
wl_set.