cases f false true <;> simp
case refl
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
n : Nat
hnk : n < 2 ^ succ k
hmk : 0 < 2 ^ succ k
⊢ (if f false true = true then n else 0) < 2 ^ succ k
case refl.false
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
n : Nat
hnk : n < 2 ^ succ k
hmk : 0 < 2 ^ succ k
⊢ 0 < 2 ^ succ k

case refl.true
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
n : Nat
hnk : n < 2 ^ succ k
hmk : 0 < 2 ^ succ k
⊢ n < 2 ^ succ k