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