ProofShape.SwapW: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_shape.bend as ProofShape
Lines 39-42 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=39&end_line=42

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

# Array.swap.go(a, ...) is (na, old) with na as perfect as a at every depth.
def SwapW(-T: Type, -a: Array<T>, -n: U32, -i: U32, -v: T, -z: Bool, -d: Nat) -> Type:
  &na:Array<T> -> &old:T -> {Array.swap.go(T, a, n, i, v, z) == (na, old) : Array<T> & T}
    & {D.full(T, na, d) == D.full(T, a, d) : Bool}

Uses (9):
  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=Exists
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=lawful-arrays@0.1.0.0/defs.bend&name=full