Word.pwv: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as Word
Lines 340-343 of bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&start_line=340&end_line=343

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

# a word known to be 2^k has value 2^k (the word stays a variable)
def pwv(+n: Nat, +k: Nat, +hk: {Nat.is_lt(k, n) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +c: Word(n), +hc: {c == pw(n, k) : Word(n)}) -> {uw(n, c) == sc(k, one) : Nat}:
  +e = L.subst(Word(n), w => {uw(n, w) == sc(k, 1n) : Nat}, pw(n, k), c, Equal.sym(Word(n), c, pw(n, k), hc), pw_val(n, k, hk))
  L.subst(Nat, o => {uw(n, c) == S.scale_binary(k, o) : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), e)

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=scale_binary
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=pw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=pw_val
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=uw