UniqueProofs.aligned_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 94-123 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=94&end_line=123

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

def aligned_unique(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +other: List<&2, Nat>, +first: Shape.Aligned(left, right, output), +second: Shape.Aligned(left, right, other)) -> {output == other : List<&2, Nat>}:
  match left right output:
    case Nil{} Nil{} Nil{}:
      match other:
        case Nil{}:
          {==}
        case oh <> ot:
          match second:
    case +lh <> +lt +rh <> +rt +oh <> +ot:
      match other:
        case Nil{}:
          match second:
        case +qh <> +qt:
          Shape.AStep{+a1, +t1} = first
          Shape.AStep{+a2, +t2} = second
          %axis_unique(lh, rh, oh, qh, a1, a2) : {oh <> ot == _ <> qt : List<&2, Nat>}
          %aligned_unique(lt, rt, ot, qt, t1, t2) : {oh <> ot == oh <> _ : List<&2, Nat>}
          {==}
    case Nil{} Nil{} oh <> ot:
      match first:
    case Nil{} rh <> rt Nil{}:
      match first:
    case lh <> lt Nil{} Nil{}:
      match first:
    case Nil{} rh <> rt oh <> ot:
      match first:
    case lh <> lt Nil{} oh <> ot:
      match first:
    case lh <> lt rh <> rt Nil{}:
      match first:

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=Aligned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned.Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=axis_unique