GatherPROOF.triple: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
Lines 459-461 of bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&start_line=459&end_line=461

import Base

def triple(-acc: F32, -x: F32, -a: Array<F32>, -b: Array<U32>, -A: Array<F32>, -B: Array<U32>, ea: {a == A : Array<F32>}, eb: {b == B : Array<U32>}) ->
  {(F32.add(acc, x), (a, b)) == (F32.add(acc, x), (A, B)) : F32 & (Array<F32> & Array<U32>)}:
  Equal.cong(Array<F32> & Array<U32>, F32 & (Array<F32> & Array<U32>), p => (F32.add(acc, x), p), (a, b), (A, B), both(a, b, A, B, ea, eb))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=both