def shift_dbl

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:351

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

351def shift_dbl(+k: Nat, +z: Nat) -> {C.shift(k, Nat.double(z)) == Nat.double(C.shift(k, z)) : Nat}:
352  match k:
353    case 0n:
354      {==}
355    case 1n+ +p:
356      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, Nat.double(z)), Nat.double(C.shift(p, z)), shift_dbl(p, z))