Add theorem that states that wl_state is always subset of wl_set.

Prove the theorem for everything except while. The verification procedure
correctness (flow_no_bug) is direct consequence of this theorem and is proved.