def internal_sorted_cons_cons_intro

bend-mathlib@0.8.1.0 · sort.bend:10

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

10def internal_sorted_cons_cons_intro(~A: Data, ~le: A -> A -> Bool, +x: A, +y: A, +t: List<&2, A>, hxy: {le(x, y) == True{} : Bool}, hyt: MList.sorted_by(~A, ~le, y <> t)) -> MList.sorted_by(~A, ~le, x <> y <> t):
11  %MList.internal_sorted_cons_true(~A, ~le, x, y, List.zip(&2, A, &2, A, y <> t, t), hxy) : {_ == True{} : Bool}
12  hyt