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

import Base

def AP.reflect(-T: Data, a: Array<T>) -> &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}:
  match a:
    case ALeaf{x}:
      (APLeaf{x}, {==})
    case ANode{xs, ys}:
      AP.reflect.join(T, xs, ys, AP.reflect(T, xs), AP.reflect(T, ys))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Exists
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.Tree
  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.reflect.join