Clone.join: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
Lines 19-35 of bendtorch-core@0.1.0.0/src/storage/clone.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&start_line=19&end_line=35

import Base

def join(-T: Data, -d: Nat, -xs: Array<T>, -ys: Array<T>,
  left: Cloned<T, d, xs>, right: Cloned<T, d, ys>) -> Cloned<T, 1n+d, ANode{xs, ys}>:
  match left:
    case Cloned{xa, xb, exact_x, same_xa, same_xb, valid_xa, valid_xb}:
      match right:
        case Cloned{ya, yb, exact_y, same_ya, same_yb, valid_ya, valid_yb}:
          Cloned{ANode{xa, ya}, ANode{xb, yb},
            Equal.trans(Array<T> & Array<T>, (ANode{xa, ya}, ANode{xb, yb}),
              Array.clone.node(T, Array.clone(T, xs), (ya, yb)),
              Array.clone.node(T, Array.clone(T, xs), Array.clone(T, ys)),
              Equal.cong(Array<T> & Array<T>, Array<T> & Array<T>,
                r => Array.clone.node(T, r, (ya, yb)), (xa, xb), Array.clone(T, xs), exact_x),
              Equal.cong(Array<T> & Array<T>, Array<T> & Array<T>,
                r => Array.clone.node(T, Array.clone(T, xs), r), (ya, yb), Array.clone(T, ys), exact_y)),
            node_equal(T, xa, ya, xs, ys, same_xa, same_ya),
            node_equal(T, xb, yb, xs, ys, same_xb, same_yb),
            (valid_xa, valid_ya), (valid_xb, valid_yb)}

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=Array.clone
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.clone.node
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=Cloned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=node_equal