def half_equal
bendtorch-core@0.1.0.0 · src/tensor/parallel_proofs.bend:181
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as ParallelProofs
import Base
181def half_equal(-S: Type, -start: S, -state: S, -half: S, -split: S -> S & S, -pick: (S & S) -> S,
182 picked: {half == pick(split(state)) : S}, at: {state == start : S}, copied: {pick(split(start)) == start : S}) ->
183 {half == start : S}:
184 Equal.trans(S, half, pick(split(start)), start,
185 Equal.trans(S, half, pick(split(state)), pick(split(start)), picked, Equal.cong(S, S, s => pick(split(s)), state, start, at)),
186 copied)