Sort.internal_sorted_cons_cons_intro: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/sort.bend as Sort
Lines 10-12 of bend-mathlib@0.8.1.0/sort.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/sort.bend&start_line=10&end_line=12

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

def 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):
  %MList.internal_sorted_cons_true(~A, ~le, x, y, List.zip(&2, A, &2, A, y <> t, t), hxy) : {_ == True{} : Bool}
  hyt

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.zip
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=internal_sorted_cons_true
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=sorted_by