ProofShape.set_full.fin: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_shape.bend as ProofShape
Lines 170-181 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=170&end_line=181

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

def set_full.fin(-T: Type, -a: Array<T>, -b: Array<T>, +n: U32, +i: U32, -v: T, +d: Nat,
  hf: {D.full(T, a, d) == True{} : Bool}, q: {b == a : Array<T>},
  w: SwapW(T, b, n, U32.and(i, U32.sub(n, 1)), v, U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)), d)) ->
  {D.full(T, Array.set.fin(T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v,
    U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)))), d) == True{} : Bool}:
  (na, old, e, f) = w
  %Equal.sym(Array<T> & T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v,
    U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n))), (na, old), e) :
    {D.full(T, Array.set.fin(T, _), d) == True{} : Bool}
  Equal.trans(Bool, D.full(T, na, d), D.full(T, b, d), True{}, f,
    Equal.trans(Bool, D.full(T, b, d), D.full(T, a, d), True{},
      Equal.cong(Array<T>, Bool, x => D.full(T, x, d), b, a, q), hf))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set.fin
  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=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Base/base.bend&name=U32.and
  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_shape.bend&name=SwapW