List.internal_head_le_mem_step: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/list.bend as List
Lines 993-999 of bend-mathlib@0.8.1.0/list.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/list.bend&start_line=993&end_line=999

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

def internal_head_le_mem_step(+x: Nat, +z: Nat, -t: List<&2, Nat>, +y: Nat, b: Bool, e: {Nat.is_eq(z, y) == b : Bool}, hxz: MNat.le(x, z), hm: {Bool.or(b, List.contains(~Nat, ~Nat.is_eq, t, y)) == True{} : Bool}, ih: {List.contains(~Nat, ~Nat.is_eq, t, y) == True{} : Bool} -> MNat.le(z, y)) -> MNat.le(x, y):
  match b:
    case True{}:
      %MNat.eq_of_is_eq(z, y, e) : MNat.le(x, _)
      hxz
    case False{}:
      MNat.le_trans(x, z, y, hxz, ih(hm))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.contains
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=eq_of_is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le_trans