Complete correctness result for simple 1D loop example.

The remaining requirement was to prove that
construct_explicit_relation only ever created (x,y) entries in its
relation where y was not too large. The final correctness result is

 |- E = construct_explicit_relation M N f g ⇒
    δ = cpack E ⇒
    N ≤ vsz A ⇒
    FOR (0,N) (λi A. update A (δ ' i) (rhs (δ ' i) (A ' (δ ' i)))) A =
    FOR (0,N) (λi A. update A i (rhs i (A ' i))) A

where ‘rhs’ is a function representing the right hand side of the
loop's (one) assignment. This function gets to combine an index and an
array element in arbitrary ways.