coq - ltac の単一出現を書き換える

Question

rewriteltac で呼び出して 1 つのオカレンスのみを書き換えるにはどうすればよいですか? coqのドキュメントに何か言及されていると思いますrewrite atが、実際に実際に使用できておらず、例もありません。

これは私がやろうとしていることの例です:

Definition f (a b: nat): nat.
Admitted.

Theorem theorem1: forall a b: nat, f a b = 4.
Admitted.

Theorem theorem2: forall (a b: nat), (f a b) + (f a b) = 8.
Proof.
intros a b.
(*
my goal here is f a b + f a b = 8
I want to only rewrite the first f a b
The following tactic call doesn't work
*)
rewrite -> theorem1 at 1.