def shift

stelliferous@0.0.2.0 · proofs/word_multiplication.bend:53

import Base

53def shift(+n: Nat,+w: Word(1n+n)) -> {Word.shl(1n+n,w) == WCon{False{},truncate(n,w)} : Word(1n+n)}:
54  WCon{+b,+t} = w
55  %put(n,b,t) : {WCon{False{},Word.shl.put(n,b,t)} == WCon{False{},_} : Word(1n+n)}
56  {==}