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

import Base
import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast

def crossed(+zero_left: Nat, +right_a: Nat, +left_b: Nat, +zero_right: Nat, +left_rank: Nat, +right_rank: Nat, +zero_a: {0n == zero_left : Nat}, zero_b: {0n == zero_right : Nat}, first: {Nat.add(zero_left, left_rank) == Nat.add(right_a, right_rank) : Nat}, second: {Nat.add(left_b, left_rank) == Nat.add(zero_right, right_rank) : Nat}) -> {zero_left == left_b : Nat}:
  +left_rank_eq = Equal.trans(Nat, left_rank, Nat.add(zero_left, left_rank), Nat.add(right_a, right_rank), Equal.cong(Nat, Nat, value => Nat.add(value, left_rank), 0n, zero_left, zero_a), first)
  +second_eq = Equal.trans(Nat, Nat.add(left_b, left_rank), Nat.add(zero_right, right_rank), right_rank, second, Equal.sym(Nat, right_rank, Nat.add(zero_right, right_rank), Equal.cong(Nat, Nat, value => Nat.add(value, right_rank), 0n, zero_right, zero_b)))
  +nested = Equal.trans(Nat, Nat.add(left_b, Nat.add(right_a, right_rank)), Nat.add(left_b, left_rank), right_rank, Equal.sym(Nat, Nat.add(left_b, left_rank), Nat.add(left_b, Nat.add(right_a, right_rank)), Equal.cong(Nat, Nat, value => Nat.add(left_b, value), left_rank, Nat.add(right_a, right_rank), left_rank_eq)), second_eq)
  +flat = Equal.trans(Nat, Nat.add(Nat.add(left_b, right_a), right_rank), Nat.add(left_b, Nat.add(right_a, right_rank)), right_rank, Equal.sym(Nat, Nat.add(left_b, Nat.add(right_a, right_rank)), Nat.add(Nat.add(left_b, right_a), right_rank), Index.add_assoc(left_b, right_a, right_rank)), nested)
  +sum = Equal.trans(Nat, Nat.add(left_b, right_a), Nat.add(Nat.add(left_b, right_a), 0n), 0n, Equal.sym(Nat, Nat.add(Nat.add(left_b, right_a), 0n), Nat.add(left_b, right_a), Broadcast.add_zero(Nat.add(left_b, right_a))), absorb(Nat.add(left_b, right_a), right_rank, flat))
  Equal.trans(Nat, zero_left, 0n, left_b, Equal.sym(Nat, 0n, zero_left, zero_a), Equal.sym(Nat, left_b, 0n, sum_zero(left_b, right_a, sum)))

Uses (9):
  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=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/broadcast_proofs.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=absorb
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=sum_zero