diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index 85ffb0334e39fa4e1f1bd9c537b0eed4406e4c6d..63fe1861086a67c7cc1583d0728d0e933eeda4b5 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -345,6 +345,55 @@ Tactic Notation "tp_cas_suc" constr(j) :=
     |pm_reflexivity || fail "tp_cas_suc: this should not happen"
     |(* new goal *)].
 
+Lemma tac_tp_faa `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc)  e2 (z1 z2 : Z) Q :
+  nclose specN ⊆ E1 →
+  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
+  envs_lookup_delete false i2 Δ1 = Some (false, j ⤇ e, Δ2)%I →
+  e = fill K' (FAA #l e2) →
+  IntoVal e2 #z2 →
+  envs_lookup i3 Δ2 = Some (false, l ↦ₛ #z1)%I →
+  envs_simple_replace i3 false
+    (Esnoc (Esnoc Enil i2 (j ⤇ fill K' #z1)) i3 (l ↦ₛ #(z1+z2))%I) Δ2 = Some Δ3 →
+  envs_entails Δ3 (|={E1,E2}=> Q) →
+  envs_entails Δ1 (|={E1,E2}=> Q).
+Proof.
+  rewrite envs_entails_eq. intros ??? Hfill <- ?? HQ.
+  rewrite -(idemp bi_and (of_envs Δ1)).
+  rewrite {1}(envs_lookup_sound' Δ1 false). 2: eassumption.
+  rewrite bi.sep_elim_l.
+  enough (<pers> spec_ctx ρ ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
+  { rewrite -bi.intuitionistically_into_persistently_1.
+    destruct p; simpl;
+    by rewrite ?(bi.intuitionistic_intuitionistically (spec_ctx ρ)). }
+  rewrite bi.persistently_and_intuitionistically_sep_l.
+  rewrite bi.intuitionistic_intuitionistically.
+  rewrite envs_lookup_delete_sound // /=.
+  rewrite (envs_simple_replace_sound Δ2 Δ3 i3) //.
+  simpl. rewrite right_id Hfill.
+  (* (S (spec_ctx ρ) (S (j => fill _ _) (S (l ↦ v) ..))) *)
+  rewrite (assoc _ (spec_ctx ρ) (j ⤇ fill K' _)%I).
+  (* (S (S (spec_ctx ρ) (j => fill _ _)) (S (l ↦ v) ..)) *)
+  rewrite assoc.
+  rewrite -(assoc _ (spec_ctx ρ) (j ⤇ fill K' _)%I).
+  rewrite step_faa //.
+  rewrite -(fupd_trans E1 E1 E2).
+  rewrite fupd_frame_r.
+  apply fupd_mono.
+  by rewrite (comm _ (j ⤇ _)%I) bi.wand_elim_r.
+Qed.
+
+Tactic Notation "tp_faa" constr(j) :=
+  iStartProof;
+  eapply (tac_tp_faa j);
+    [solve_ndisj || fail "tp_faa: cannot prove 'nclose specN ⊆ ?'"
+    |iAssumptionCore || fail "tp_faa: cannot find spec_ctx" (* spec_ctx *)
+    |iAssumptionCore || fail "tp_faa: cannot find '" j " ⤇ ?'"
+    |tp_bind_helper (* e = K'[CAS _ _ _] *)
+    |iSolveTC (* IntoVal *)
+    |iAssumptionCore || fail "tp_faa: cannot find '? ↦ ?'"
+    |pm_reflexivity || fail "tp_faa: this should not happen"
+    |(* new goal *)].
+
 Lemma tac_tp_fork `{relocG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e' Q :
   nclose specN ⊆ E1 →
   envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 198cc4df27f228cfa858d66dab727307f9cc1ee1..e79dd2fb436fab3f5eebc4d186c93d7a4b3fc5bc 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -248,6 +248,25 @@ Section rules.
     by iApply "Hlog".
   Qed.
 
+  Lemma refines_faa_r Γ E K l e2 (i1 i2 : Z) t A :
+    nclose specN ⊆ E →
+    IntoVal e2 #i2 →
+    l ↦ₛ #i1 -∗
+    (l ↦ₛ #(i1+i2) -∗ {E;Γ} ⊨ t << fill K (of_val #i1) : A)
+    -∗ {E;Γ} ⊨ t << fill K (FAA #l e2) : A.
+  Proof.
+    iIntros (?<-) "Hl Hlog".
+    pose (Φ := (fun w => ⌜w = #i1⌝ ∗ l ↦ₛ #(i1+i2))%I).
+    iApply (refines_step_r Φ with "[Hl]"); eauto.
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=".
+      tp_faa j; auto.
+      iExists #i1. simpl.
+      iFrame. eauto. }
+    iIntros (w) "[% Hl]"; subst.
+    by iApply "Hlog".
+  Qed.
+
   Lemma refines_fork_r Γ E K (e t : expr) A
    (Hmasked : nclose specN ⊆ E)
    (Hclosed : is_closed_expr [] e) :
@@ -451,4 +470,16 @@ Section rules.
       iSpecialize ("Hlog" with "[]"); eauto.
   Qed.
 
+  Lemma refines_faa_l K Γ E l e2 (i2 : Z) t A :
+    IntoVal e2 #i2 →
+    (|={⊤,E}=> ∃ (i1 : Z), ▷ l ↦ #i1 ∗
+     ▷ (l ↦ #(i1 + i2) -∗ {E;Γ} ⊨ fill K (of_val #i1) << t : A))
+    -∗ Γ ⊨ fill K (FAA #l e2) << t : A.
+  Proof.
+    iIntros (<-) "Hlog".
+    iApply refines_atomic_l; auto.
+    iMod "Hlog" as (i1) "[Hl Hlog]". iModIntro.
+    by iApply (wp_faa with "Hl").
+  Qed.
+
 End rules.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index b88f75355ee2d69bdf6491187dd196a0c89a1ecd..34df826dd5c685fccbe47c5c6fe51871afac51e9 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -169,7 +169,7 @@ Section rules.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
   Qed.
 
-  (** CAS & FAI *)
+  (** CAS & FAA *)
   Lemma step_cas_fail E ρ j K l q v' e1 v1 e2 v2 :
     IntoVal e1 v1 →
     IntoVal e2 v2 →
@@ -225,31 +225,7 @@ Section rules.
     left; eauto.
   Qed.
 
-  Lemma step_fork E ρ j K e :
-    nclose specN ⊆ E →
-    spec_ctx ρ ∗ j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K #() ∗ j' ⤇ e.
-  Proof.
-    iIntros (?) "[#Hspec Hj]".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
-    iInv specN as (tp σ) ">[Hown %]" "Hclose".
-    iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
-    assert (j < length tp)%nat by eauto using lookup_lt_Some.
-    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
-    { by eapply auth_update, prod_local_update_1,
-        singleton_local_update, (exclusive_local_update _ (Excl (fill K #()))). }
-    iMod (own_update with "Hown") as "[Hown Hfork]".
-    { eapply auth_update_alloc, prod_local_update_1,
-        (alloc_singleton_local_update _ (length tp) (Excl e)); last done.
-      rewrite lookup_insert_ne ?tpool_lookup; last lia.
-      by rewrite lookup_ge_None_2. }
-    iExists (length tp). iFrame "Hj Hfork". iApply "Hclose". iNext.
-    iExists (<[j:=fill K #()]> tp ++ [e]), σ.
-    rewrite to_tpool_snoc insert_length to_tpool_insert //. iFrame. iPureIntro.
-    eapply rtc_r, step_insert; eauto. econstructor; eauto.
-  Qed.
-
-  Lemma step_fai E ρ j K l e1 e2 (i1 i2 : Z) :
+  Lemma step_faa E ρ j K l e1 e2 (i1 i2 : Z) :
     IntoVal e1 #i2 →
     nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (FAA #l e1) ∗ l ↦ₛ #i1
@@ -275,5 +251,30 @@ Section rules.
     eapply rtc_r, step_insert_no_fork; eauto. simpl. econstructor; eauto.
   Qed.
 
+  (** Fork *)
+  Lemma step_fork E ρ j K e :
+    nclose specN ⊆ E →
+    spec_ctx ρ ∗ j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K #() ∗ j' ⤇ e.
+  Proof.
+    iIntros (?) "[#Hspec Hj]".
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
+    iInv specN as (tp σ) ">[Hown %]" "Hclose".
+    iDestruct (own_valid_2 with "Hown Hj")
+      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+    assert (j < length tp)%nat by eauto using lookup_lt_Some.
+    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
+    { by eapply auth_update, prod_local_update_1,
+        singleton_local_update, (exclusive_local_update _ (Excl (fill K #()))). }
+    iMod (own_update with "Hown") as "[Hown Hfork]".
+    { eapply auth_update_alloc, prod_local_update_1,
+        (alloc_singleton_local_update _ (length tp) (Excl e)); last done.
+      rewrite lookup_insert_ne ?tpool_lookup; last lia.
+      by rewrite lookup_ge_None_2. }
+    iExists (length tp). iFrame "Hj Hfork". iApply "Hclose". iNext.
+    iExists (<[j:=fill K #()]> tp ++ [e]), σ.
+    rewrite to_tpool_snoc insert_length to_tpool_insert //. iFrame. iPureIntro.
+    eapply rtc_r, step_insert; eauto. econstructor; eauto.
+  Qed.
+
 End rules.