Weaken precondition of `balanceL` to prepare for deletion
Weaken precondition of `balanceL` to prepare for deletion

look, no proofs have to change, neither in `balanceL` nor where it is
used (but omega certainly did not get faster).

antalsz/hs-to-coq,antalsz/hs-to-coq