removing lemma_not_empty and lemma_not_zero

[doublec]

I wondered why lemma_not_empty and lemma_not_zero is needed since you have the if that should narrow down the constraint:

if length(s) > 0 && pad > 0

If you use nested if's, checking each boolean separately then you don't need the lemma. I asked Hongwei about this once and he said:

'&&' is a macro (due to shortcut evaluation); it is not given a dependent type. Replacing '&&' with * (bmul) should work, though.

Replacing the 'if' with:

if (length(s) > 0) * (pad > 0)

does allow type checking if the lemmas are removed. Just noting this as to why the lemmas are needed and why ATS2 isn't computing it itself.