def sc_idx

bend-collections-laws-math@1.0.0.0 · proofs/lib/arith.bend:143

import Base

143# 2^(k + j) x == 2^k (2^j x)
144def sc_idx(+k: Nat, +j: Nat, +x: Nat) -> {sc(Nat.add(k, j), x) == sc(k, sc(j, x)) : Nat}:
145  match k:
146    case 0n:
147      {==}
148    case 1n+p:
149      Equal.cong(Nat, Nat, Nat.double, sc(Nat.add(p, j), x), sc(p, sc(j, x)), sc_idx(p, j, x))