def shift_comp

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

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

184def shift_comp(+a: Nat, +b: Nat, +x: Nat) -> {C.shift(Nat.add(a, b), x) == C.shift(a, C.shift(b, x)) : Nat}:
185  match a:
186    case 0n:
187      {==}
188    case 1n+ +p:
189      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(Nat.add(p, b), x), C.shift(p, C.shift(b, x)), shift_comp(p, b, x))