def internal_sorted_tail

bend-mathlib@0.8.1.0 · sort.bend:34

import Base
import bend-mathlib@0.8.1.0/list.bend as MList

34def internal_sorted_tail(~A: Data, ~le: A -> A -> Bool, +x: A, +xs: List<&2, A>, h: MList.sorted_by(~A, ~le, x <> xs)) -> MList.sorted_by(~A, ~le, xs):
35  match xs:
36    case Nil{}:
37      {==}
38    case +y <> +t:
39      internal_sorted_cons_cons_elim_tail(~A, ~le, x, y, t, h)