ParallelProofs.half_equal: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as ParallelProofs
Lines 181-186 of bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&start_line=181&end_line=186

import Base

def half_equal(-S: Type, -start: S, -state: S, -half: S, -split: S -> S & S, -pick: (S & S) -> S,
  picked: {half == pick(split(state)) : S}, at: {state == start : S}, copied: {pick(split(start)) == start : S}) ->
  {half == start : S}:
  Equal.trans(S, half, pick(split(start)), start,
    Equal.trans(S, half, pick(split(state)), pick(split(start)), picked, Equal.cong(S, S, s => pick(split(s)), state, start, at)),
    copied)

Uses (3):
  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.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair