UniqueProofs.axis_unique: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend as UniqueProofs
Lines 73-92 of bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&start_line=73&end_line=92

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

def axis_unique(-left: Nat, -right: Nat, -output: Nat, -other: Nat, +first: Shape.Axis<left, right, output>, +second: Shape.Axis<left, right, other>) -> {output == other : Nat}:
  match first second:
    case Shape.AxisEqual{l1, r1} Shape.AxisEqual{l2, r2}:
      Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))
    case Shape.AxisEqual{l1, r1} Shape.AxisLeftOne{o2, r2}:
      Equal.trans(Nat, output, right, other, r1, Equal.sym(Nat, other, right, r2))
    case Shape.AxisEqual{l1, r1} Shape.AxisRightOne{l2, o2}:
      Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))
    case Shape.AxisLeftOne{o1, r1} Shape.AxisEqual{l2, r2}:
      Equal.trans(Nat, output, right, other, r1, Equal.sym(Nat, other, right, r2))
    case Shape.AxisLeftOne{o1, r1} Shape.AxisLeftOne{o2, r2}:
      Equal.trans(Nat, output, right, other, r1, Equal.sym(Nat, other, right, r2))
    case Shape.AxisLeftOne{o1, r1} Shape.AxisRightOne{l2, o2}:
      Equal.trans(Nat, output, 1n, other, Equal.trans(Nat, output, right, 1n, r1, Equal.sym(Nat, 1n, right, o2)), Equal.trans(Nat, 1n, left, other, o1, Equal.sym(Nat, other, left, l2)))
    case Shape.AxisRightOne{l1, o1} Shape.AxisEqual{l2, r2}:
      Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))
    case Shape.AxisRightOne{l1, o1} Shape.AxisLeftOne{o2, r2}:
      Equal.trans(Nat, output, 1n, other, Equal.trans(Nat, output, left, 1n, l1, Equal.sym(Nat, 1n, left, o2)), Equal.trans(Nat, 1n, right, other, o1, Equal.sym(Nat, other, right, r2)))
    case Shape.AxisRightOne{l1, o1} Shape.AxisRightOne{l2, o2}:
      Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Axis