intro i
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f n n) i = getBit 0 i
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n i : Nat
⊢ getBit (bitwise f n n) i = getBit 0 i