Progress in the proof of the invariant.

Was surprised not to find very basic lemmas on lattices:
l1 \_/ l2 = l2 \_/ l1.
isLow (l1 \_/ l2) l = isLow l1 l && isLow l2 l.

I'm probably not looking at the right place. Reproving them didn't take long
anyway.