def both
bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:248
import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
import Base
248def both(-a: Array<F32>, -b: Array<U32>, -A: Array<F32>, -B: Array<U32>, ea: {a == A : Array<F32>}, eb: {b == B : Array<U32>}) ->
249 {(a, b) == (A, B) : Array<F32> & Array<U32>}:
250 Equal.trans(Array<F32> & Array<U32>, (a, b), (A, b), (A, B),
251 Equal.cong(Array<F32>, Array<F32> & Array<U32>, x => (x, b), a, A, ea),
252 Equal.cong(Array<U32>, Array<F32> & Array<U32>, y => (A, y), b, B, eb))