Proof step 12 from proof exactarray-02-01 (previous step)

⊦ r = r0, exactarray(refval(r), ty, i, st[r0 -- sk, val0]) ↔ exactarray(refval(r), ty, i, st), is_classtype(ty), is_arraytype(ty)

User applied rule insert rewrite lemma

Proof step 1:
⊦ exactarray(val, ty, i, st) ↔ exactreftype(val, mkarraytype(ty), st) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st ∧ is_arrayref(val .refval, i, st)
Proof step 11:
⊦ r = r0, exactreftype(refval(r), mkarraytype(ty), st[r0 -- sk, val0]) ∧ refval(r) .refval ≠ jvmref ∧ (refval(r) .refval -- _length) × intval(i) ∈ st[r0 -- sk, val0] ∧ is_arrayref(refval(r) .refval, i, st[r0 -- sk, val0]) ↔ exactarray(refval(r), ty, i, st), is_classtype(ty), is_arraytype(ty)

[crewrite-arg: exactarray-01 , F , [st, i, ty, val] → [st[r0 -- sk, val0], i, ty, refval(r)] ]

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[r0 -- sk, val0], i, ty, refval(r))]]