UniqueProofs.broadcast_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 130-141 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=130&end_line=141

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

def broadcast_unique(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +other: List<&2, Nat>, +first: Shape.Broadcast<left, right, output>, +second: Shape.Broadcast<left, right, other>) -> {output == other : List<&2, Nat>}:
  match first:
    case Shape.BAlign{+lp1, +rp1, +m1, +a1}:
      match second:
        case Shape.BAlign{+lp2, +rp2, +m2, +a2}:
          +left_rank = List.length(&2, Nat, left)
          +right_rank = List.length(&2, Nat, right)
          +e1 = balance(lp1, rp1, left, right, output, a1)
          +e2 = balance(lp2, rp2, left, right, other, a2)
          +same_left = left_padding_equal(lp1, rp1, lp2, rp2, left_rank, right_rank, m1, m2, e1, e2)
          +same_right = cancel_right(rp1, rp2, right_rank, Equal.trans(Nat, Nat.add(rp1, right_rank), Nat.add(lp1, left_rank), Nat.add(rp2, right_rank), Equal.sym(Nat, Nat.add(lp1, left_rank), Nat.add(rp1, right_rank), e1), Equal.trans(Nat, Nat.add(lp1, left_rank), Nat.add(lp2, left_rank), Nat.add(rp2, right_rank), Equal.cong(Nat, Nat, value => Nat.add(value, left_rank), lp1, lp2, same_left), e2)))
          aligned_unique(Shape.pad(lp1, left), Shape.pad(rp1, right), output, other, a1, retype(lp1, lp2, rp1, rp2, left, right, other, same_left, same_right, a2))

Uses (14):
  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.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=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Broadcast
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=pad
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=aligned_unique
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=balance
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=cancel_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=left_padding_equal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=retype