ProofTree.mirror: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_tree.bend as ProofTree
Lines 48-53 of lawful-arrays@0.1.0.0/proof_tree.bend: https://jend.leeeet.dev/read.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&start_line=48&end_line=53

import Base

def mirror(-T: Data, a: Array<T>) -> Mirror(T, a):
  match a:
    case ALeaf{x}:
      (TLeaf{x}, {==})
    case ANode{xs, ys}:
      mirror.node(T, xs, ys, mirror(T, xs), mirror(T, ys))

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=Mirror
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=mirror.node