def internal_sorted_cons_cons_elim_le

bend-mathlib@0.8.1.0 · sort.bend:28

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

28def internal_sorted_cons_cons_elim_le(~A: Data, ~le: A -> A -> Bool, +x: A, +y: A, +t: List<&2, A>, h: MList.sorted_by(~A, ~le, x <> y <> t)) -> {le(x, y) == True{} : Bool}:
29  internal_sorted_le_step(~A, ~le, x, y, t, le(x, y), {==}, h)