Are there special considerations for conjunctions and other basic (or otherwise) logical operators when they are included as arguments to functions? Currently I am running into a wall on a proof that may be characterized by the failure of the folowing result. The conjecture
lemma "f ( P & Q ) ==> f ( Q & P )"
will not be proved by simp, auto, or blast, but
lemma "P & Q ==> Q & P" by auto
is evaluated without complaint.
Am I missing something basic? Any thoughts on this question would be appreciated.