shorten vtoclg, vtoclegft, vtoclf

[wlammen]

1. Shorten vtoclg by moving vtocleg before it, and using it.
2. Shorten vtoclf by moving vtoclef before it, and using it.
3. Shorten vtoclegft. It is a degenerate case of ceqsalt, so basing the proof on it saves 2 proof bytes.
4. Use elissetv in clelab and elex22, following the comment in elissetv.
5. Update the comment of vtoclg1f to point out its current difference to vtoclgf
6. Extract a subproof of vtoclgft with minor modifications to arrive at wl-issetft in my mathbox. I'd rather see it in Main, but so far vtoclgft would be its only user, cutting down its proof size. So for now I'll keep it in my Mathbox.