Solution for Arrays.Realization.hseg_focus
introv Hk. forwards* (l1&x&l2&->&<-): LibList.list_middle_inv k L.
xchange hseg_app. xchange hseg_cons. rewrite* LibList.nth_middle.
simpl. xsimpl. intros w. xchange <- hseg_cons. xchange <- hseg_app.
rewrite* LibList.update_middle. { rew_list*. } { applys Inhab_val. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
