PROOF.AP.len_take: def of bend-osdev-array@0.1.0.1
Import: import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
Lines 1401-1411 of bend-osdev-array@0.1.0.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&start_line=1401&end_line=1411

import Base

# a list of n + m elements cut after n: n, then m elements
def AP.len_take(-T: Data, xs: List<&2, T>, n: Nat, -m: Nat, h: {List.length(&2, T, xs) == Nat.add(n, m) : Nat}) -> {List.length(&2, T, List.take(&2, T, xs, n)) == n : Nat}:
  match xs n:
    case Nil{} 0n:
      {==}
    case Nil{} 1n+p:
      Empty.absurd({List.length(&2, T, List.take(&2, T, Nil{}, 1n+p)) == 1n+p : Nat}, AP.sz(Nat.add(p, m), Equal.sym(Nat, 0n, 1n+Nat.add(p, m), h)))
    case Con{x, t} 0n:
      {==}
    case Con{x, t} 1n+p:
      AP.succ_cong(List.length(&2, T, List.take(&2, T, t, p)), p, AP.len_take(T, t, p, m, AP.pred_cong(List.length(&2, T, t), Nat.add(p, m), h)))

Uses (10):
  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.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.pred_cong
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.succ_cong
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.sz