Proof step 19 from proof okarray-put-08 (previous step)

⊦ fs ' = _length, fs ' = _type, okarray(val, ty, i, st[r -- fs ', val0]) ↔ okarray(val, ty, i, st)

User applied rule insert rewrite lemma

Proof step 2:
⊦ okarray(val, ty, i, st) ↔ okreftype(val, mkarraytype(ty), st) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st ∧ 0 ≤ i ∧ is_arrayref(val .refval, i, st) ∧ (∀ j. 0 ≤ j ∧ j < i → oktype(st[val .refval -- j '], ty, st))
Proof step 18:
⊦ fs ' = _length, fs ' = _type, okreftype(val, mkarraytype(ty), st[r -- fs ', val0]) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st[r -- fs ', val0] ∧ 0 ≤ i ∧ is_arrayref(val .refval, i, st[r -- fs ', val0]) ∧ (∀ j. 0 ≤ j ∧ j < i → oktype(st[r -- fs ', val0][val .refval -- j '], ty, st[r -- fs ', val0])) ↔ okarray(val, ty, i, st)

[crewrite-arg: okarrayOfLength , F , [st, i, ty, val] → [st[r -- fs ', val0], i, ty, val] ]

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[r -- fs ', val0], i, ty, val)]]