law shift_power

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:48

import Base

48law shift_power:
49  for +width: Nat
50  for +depth: Nat
51  {Word.shl(width,power(width,depth)) == power(width,1n+depth) : Word(width)}