apply Nat.bitext
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = b
n : Nat
⊢ bitwise f n n = n
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = b
n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f n n) i = getBit n i