We prove the key lemma that
        ( I, I1, I2: Nat, A : Arr)
                I1 <= I2   implies   (I1 || put(I, I2, A)) R (I1 || A) .
We use induction on NAT, with the signature {0,s}.

Induction requires that we do the following:

  1. base case: prove the assertion for 0.
  2. induction step: prove the assertion for s n, assuming it for n.

21 December 1996