PROOF.AP.of_list_eq: def of bend-osdev-array@0.1.0.1
Import: import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
Lines 1347-1357 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=1347&end_line=1357

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

def AP.of_list_eq(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> {A.Arrays.of_list(T, d, xs, f) == AP.build(T, AP.tof(T, d, xs, f)) : Array<T>}:
  match d:
    case 0n:
      {==}
    case 1n+ +p:
      +s = A.Arrays.slots(p)
      +l = List.take(&2, T, xs, s)
      +r = List.drop(&2, T, xs, s)
      %Equal.sym(Array<T>, A.Arrays.of_list(T, p, l, f), AP.build(T, AP.tof(T, p, l, f)), AP.of_list_eq(T, p, l, f)) : {ANode{_, A.Arrays.of_list(T, p, r, f)} == ANode{AP.build(T, AP.tof(T, p, l, f)), AP.build(T, AP.tof(T, p, r, f))} : Array<T>}
      %Equal.sym(Array<T>, A.Arrays.of_list(T, p, r, f), AP.build(T, AP.tof(T, p, r, f)), AP.of_list_eq(T, p, r, f)) : {ANode{AP.build(T, AP.tof(T, p, l, f)), _} == ANode{AP.build(T, AP.tof(T, p, l, f)), AP.build(T, AP.tof(T, p, r, f))} : Array<T>}
      {==}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  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.drop
  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=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.build
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.tof
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.slots