MatmulPROOF.second_equal: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulPROOF
Lines 1045-1046 of bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&start_line=1045&end_line=1046

import Base

def second_equal(+a: U32, +b: U32, +x: U32, +y: U32, same: {[a, b] == [x, y] : List<&2, U32>}) -> {b == y : U32}:
  Equal.cong(List<&2, U32>, U32, values => Maybe.default(&2, U32, List.get(&2, U32, values, 1n), 0), [a, b], [x, y], same)

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.default
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32