diff --git a/theories/stacked_borrows/logical_state.v b/theories/stacked_borrows/logical_state.v
index 06e4ba706051bec9298ab32802a2bea61e1aa8fa..e622cb81ff955c832cf902186291663e25a7e982 100644
--- a/theories/stacked_borrows/logical_state.v
+++ b/theories/stacked_borrows/logical_state.v
@@ -807,7 +807,7 @@ Section tainted_tags.
 
   Lemma tag_tainted_interp_alloc σ l n :
     let nt := Tagged σ.(snp) in
-    tag_tainted_interp σ ⊢ tag_tainted_interp (mkState (init_mem l n σ.(shp)) (init_stacks σ.(sst) l n nt) σ.(scs) (S σ.(snp)) σ.(snc)).
+    tag_tainted_interp σ -∗ tag_tainted_interp (mkState (init_mem l n σ.(shp)) (init_stacks σ.(sst) l n nt) σ.(scs) (S σ.(snp)) σ.(snc)).
   Proof.
     intros nt. iIntros "Htainted".
     iApply (tag_tainted_interp_preserve σ with "Htainted"). { simpl. lia. }