List.sc_take_split: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend as List
Lines 356-366 of bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend&start_line=356&end_line=366

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC

def sc_take_split(-A: Data, +xs: List<&2, A>, +l: Nat, +r: Nat, +h: {Nat.is_le(l, r) == True{} : Bool}) -> {SC.take(A, xs, r) == SC.append(A, SC.take(A, xs, l), SC.take(A, SC.drop(A, xs, l), Nat.sub(r, l))) : List<&2, A>}:
  match xs l r:
    case Nil{} _ _:
      {==}
    case Con{a, t} 0n r:
      %Equal.sym(Nat, Nat.sub(r, 0n), r, sub_zero_eq(r)) : {SC.take(A, Con{a, t}, r) == SC.take(A, Con{a, t}, _) : List<&2, A>}
      {==}
    case Con{a, t} 1n+k 0n:
      Empty.absurd({SC.take(A, Con{a, t}, 0n) == SC.append(A, SC.take(A, Con{a, t}, 1n+k), SC.take(A, SC.drop(A, Con{a, t}, 1n+k), Nat.sub(0n, 1n+k))) : List<&2, A>}, L.false_true(h))
    case Con{a, t} 1n+k 1n+s:
      cons_cong(A, a, SC.take(A, t, s), SC.append(A, SC.take(A, t, k), SC.take(A, SC.drop(A, t, k), Nat.sub(s, k))), sc_take_split(A, t, k, s, h))

Uses (13):
  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.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend&name=cons_cong
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend&name=sub_zero_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=drop
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=take