simp
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ getBit (bitwise f 0 n) zero = f (getBit 0 zero) (getBit n zero)
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ getBit (bitwise f 0 n) 0 = f false (getBit n 0)