unfold bitwise
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ bitwise f m 0 / 2 = bitwise f (m / 2) (0 / 2)
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ (if m = 0 then if f false true = true then 0 else 0
      else
        if 0 = 0 then if f true false = true then m else 0
        else
          let n' := m / 2;
          let m' := 0 / 2;
          let b₁ := m % 2 = 1;
          let b₂ := 0 % 2 = 1;
          let r := bitwise f n' m';
          if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) /
      2 =
    if m / 2 = 0 then if f false true = true then 0 / 2 else 0
    else
      if 0 / 2 = 0 then if f true false = true then m / 2 else 0
      else
        let n' := m / 2 / 2;
        let m' := 0 / 2 / 2;
        let b₁ := m / 2 % 2 = 1;
        let b₂ := 0 / 2 % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r