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

import Base

def internal_least_intro(~A: Data, ~le: A -> A -> Bool, +lo: A, +h: A, +t: List<&2, A>, hh: {le(lo, h) == True{} : Bool}, ht: internal_least(~A, ~le, lo, t)) -> internal_least(~A, ~le, lo, h <> t):
  %Equal.sym(Bool, le(lo, h), True{}, hh) : {Bool.and(_, internal_all_ge(~A, ~le, lo, t)) == True{} : Bool}
  ht

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_all_ge
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_least