UniqueProofs.left_padding_equal: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend as UniqueProofs
Lines 62-71 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=62&end_line=71

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

def left_padding_equal(+lp1: Nat, +rp1: Nat, +lp2: Nat, +rp2: Nat, +left_rank: Nat, +right_rank: Nat, +m1: Shape.PadMinimal<lp1, rp1>, +m2: Shape.PadMinimal<lp2, rp2>, +first: {Nat.add(lp1, left_rank) == Nat.add(rp1, right_rank) : Nat}, +second: {Nat.add(lp2, left_rank) == Nat.add(rp2, right_rank) : Nat}) -> {lp1 == lp2 : Nat}:
  match m1 m2:
    case Shape.PLeftZero{z1} Shape.PLeftZero{z2}:
      Equal.trans(Nat, lp1, 0n, lp2, Equal.sym(Nat, 0n, lp1, z1), z2)
    case Shape.PRightZero{z1} Shape.PRightZero{z2}:
      cancel_right(lp1, lp2, left_rank, Equal.trans(Nat, Nat.add(lp1, left_rank), right_rank, Nat.add(lp2, left_rank), unpadded(lp1, rp1, left_rank, right_rank, z1, first), Equal.sym(Nat, Nat.add(lp2, left_rank), right_rank, unpadded(lp2, rp2, left_rank, right_rank, z2, second))))
    case Shape.PLeftZero{z1} Shape.PRightZero{z2}:
      crossed(lp1, rp1, lp2, rp2, left_rank, right_rank, z1, z2, first, second)
    case Shape.PRightZero{z1} Shape.PLeftZero{z2}:
      Equal.sym(Nat, lp2, lp1, crossed(lp2, rp2, lp1, rp1, left_rank, right_rank, z2, z1, second, first))

Uses (8):
  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=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=PadMinimal
  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=crossed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=unpadded