intro m n
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
this : flip f = f
⊢ ∀ {m n : Nat}, bitwise f m n = bitwise f n m
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
this : flip f = f
m n : Nat
⊢ bitwise f m n = bitwise f n m