Add theorem that wlstate can never have duplicate elements.

Proved for everything other than while.