def internal_sorted_cons_cons_elim_tail

bend-mathlib@0.8.1.0 · sort.bend:31

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

31def internal_sorted_cons_cons_elim_tail(~A: Data, ~le: A -> A -> Bool, +x: A, +y: A, +t: List<&2, A>, h: MList.sorted_by(~A, ~le, x <> y <> t)) -> MList.sorted_by(~A, ~le, y <> t):
32  internal_sorted_tail_step(~A, ~le, x, y, t, le(x, y), {==}, h)