have : flip f = f := funext (λ a => funext (λ b => h b a))
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
⊢ ∀ {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