Wp check Sorted

theorem wp_checkSorted (v vacc : Val) (l : List Int) (Φ : Val → IProp GF) :    isList (GF := GF) v l -∗    ⌜List.Pairwise (· ≤ ·) l⌝ -∗    ⌜vacc = hl_val(none()) ∨ ∃ va : Int, vacc = hl_val(some(#va)) ∧ ∀ lv ∈ l, va ≤ lv⌝ -∗    (∀ bv, isList v l -∗ ⌜bv = hl_val(#true)⌝ -∗ Φ bv) -∗    WP hl(&checkSorted &vacc &v) {{ Φ }} := by  iintro H %hsorted %hinv HΦ  iloeb as IH generalizing %vacc %l %v %hsorted %hinv  wp_rec; wp_pures  cases l with  | nil =>    icases isList_nil $$ H with %heq; subst heq    wp_pures    imodintro    iapply HΦ $$ H    itrivial  | cons hd tl =>    icases isList_cons $$ H with ⟨%loc, %tlv, %heq, Hpt, Htl⟩    subst heq    wp_pures    wp_bind !_    iapply wp_load $$ Hpt    iintro !> Hpt    rcases hinv with rfl | ⟨va, rfl, hva⟩    · wp_pures      iapply IH $$ %_ %tl %_ %((List.pairwise_cons.mp hsorted).2)        %(Or.inr ⟨hd, rfl, fun lv h => (List.pairwise_cons.mp hsorted).1 lv h⟩) Htl      iintro %bv Hl %hb      iapply HΦ $$ [Hpt Hl]      · rw [isList]        iexists loc, tlv        iframe        itrivial      itrivial    · wp_pures      rw [decide_eq_true (hva hd List.mem_cons_self)]      wp_pures      iapply IH $$ %_ %tl %_ %((List.pairwise_cons.mp hsorted).2)        %(.inr ⟨hd, rfl, (List.pairwise_cons.mp hsorted).1⟩) Htl      iintro %bv Hl %hb      iapply HΦ $$ [Hpt Hl]      · rw [isList]        iexists loc, tlv        iframe        itrivial      itrivial