Sort.internal_sorted_tail_step: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/sort.bend as Sort
Lines 21-26 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=21&end_line=26

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

def internal_sorted_tail_step(~A: Data, ~le: A -> A -> Bool, -x: A, +y: A, +t: List<&2, A>, b: Bool, e: {le(x, y) == b : Bool}, h: MList.sorted_by(~A, ~le, x <> y <> t)) -> MList.sorted_by(~A, ~le, y <> t):
  match b:
    case True{}:
      Equal.trans(Bool, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), List.zip(&2, A, &2, A, y <> t, t)), List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), (x, y) <> List.zip(&2, A, &2, A, y <> t, t)), True{}, MList.internal_sorted_cons_true(~A, ~le, x, y, List.zip(&2, A, &2, A, y <> t, t), e), h)
    case False{}:
      Empty.absurd(MList.sorted_by(~A, ~le, y <> t), MNat.internal_false_ne_true(Equal.trans(Bool, False{}, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), (x, y) <> List.zip(&2, A, &2, A, y <> t, t)), True{}, MList.internal_sorted_cons_false(~A, ~le, x, y, List.zip(&2, A, &2, A, y <> t, t), e), h)))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.all
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.zip
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=internal_sorted_cons_false
  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
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=internal_false_ne_true