Comment by shiandow

Having to replace wip with qed when indentation makes it clear it's the only thing that fits is a bit tedious.