Changed the binding invariant to use sequence truncation rather than domain restriction (which is incorrect).
Forgot to modulate.
Invariant was off by one.
Updated loop invariant.
Discharged some proofs.