def bit_bit

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbits.bend:23

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

23def bit_bit(+n: Nat) -> {C.bit(C.bit(n)) == C.bit(n) : Nat}:
24  match n:
25    case 0n:
26      {==}
27    case 1n:
28      {==}
29    case 2n+ +q:
30      bit_bit(q)