ProofShape.swap_w.hi: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_shape.bend as ProofShape
Lines 106-120 of lawful-arrays@0.1.0.0/proof_shape.bend: https://jend.leeeet.dev/read.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&start_line=106&end_line=120

import Base
import lawful-arrays@0.1.0.0/defs.bend as D
import lawful-arrays@0.1.0.0/proof_base.bend as B

def swap_w.hi(-T: Type, xs: Array<T>, -ys: Array<T>, +n: U32, +i: U32, -v: T, +d: Nat,
  w: SwapW(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v, U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n))), B.pred(d))) ->
  SwapW(T, ANode{xs, ys}, n, i, v, False{}, d):
  match d:
    case 0n:
      (na, old, e, q) = w
      (ANode{xs, na}, old,
        hi_eq(T, xs, Array.swap.go(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v,
          U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), na, old, e), {==})
    case 1n+p:
      (na, old, e, q) = w
      (ANode{xs, na}, old,
        hi_eq(T, xs, Array.swap.go(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v,
          U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), na, old, e),
        and_eq_r(D.full(T, xs, p), D.full(T, na, p), D.full(T, ys, p), q))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.swap.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/defs.bend&name=full
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=pred
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&name=SwapW
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&name=and_eq_r
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&name=hi_eq