Solution for Arrays.Realization.harray_focus_read
introv Hi. xchange* (harray_focus i). xsimpl.
xchange (hforall_specialize (nth (abs i) L)).
rewrite* LibList.update_nth_same. math.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
