Research proof index

Returns a boolean witnessing the sortedness of a HeapLang list. acc is an option of the last value in the list. -/ def checkSorted : Val := hl_val% rec check acc l := match l with | none() => #true | some(x) => let p := !x; let head := fst(p); let tail := snd(p); let ok := (match acc with | none() => #true | some(v) => v ≤ head); ok && check (some(head)...