ProofTree.mirror.node: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_tree.bend as ProofTree
Lines 42-46 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=42&end_line=46

import Base

def mirror.node(-T: Data, -xs: Array<T>, -ys: Array<T>, m1: Mirror(T, xs), m2: Mirror(T, ys))
  -> Mirror(T, ANode{xs, ys}):
  (t1, e1) = m1
  (t2, e2) = m2
  (TNode{t1, t2}, anode_eq(T, fromT(T, t1), fromT(T, t2), xs, ys, e1, e2))

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=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=anode_eq
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=fromT