How to use rewrite in subexpression of current target

Question

In coq, is it possible to somehow apply a lemma or hypothesis to a subexpression of the current goal? For example, I would like to apply the fact that the plus is commutative in order to swap 3 and 4 in this example.

Require Import Coq.Arith.Plus. Inductive foobar : nat -> Prop := | foob : forall n:nat, foobar n. Goal foob (3 + 4) = foob (4 + 3). Proof. apply plus_comm. (* or maybe rewrite plus_comm *) 

gives:

 Error: Impossible to unify "?199 + ?200 = ?200 + ?199" with "foob (3 + 4) = foob (4 + 3)". 

How can I tell coq where exactly plus_comm is used for this purpose?

Answer 1

Using simpl tactics works, but don't ask me why rewrite plus_comm or rewrite (plus_comm 3 4) doesn't work. apply are consequences, not equations.