diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index a8ee8356882111b573d355b62bf933e3ca0821ae..02d79e6f9d77eaa9a00300ad647fc6c4ea616234 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -134,7 +134,7 @@ Record always_modality_mixin {PROP : bi} (M : PROP → PROP)
     | AIEnvForall C => ∀ P, C P → P ⊢ M P
     | AIEnvTransform C => (∀ P Q, C P Q → P ⊢ M Q)
     | AIEnvClear => ∀ P, Absorbing (M P)
-    | AIEnvId => False
+    | AIEnvId => ∀ P, P ⊢ M P
     end;
   always_modality_mixin_emp : emp ⊢ M emp;
   always_modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
@@ -175,8 +175,8 @@ Section always_modality.
   Lemma always_modality_spatial_clear P :
     always_modality_spatial_spec M = AIEnvClear → Absorbing (M P).
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_id :
-    always_modality_spatial_spec M ≠ AIEnvId.
+  Lemma always_modality_spatial_id P :
+    always_modality_spatial_spec M = AIEnvId → P ⊢ M P.
   Proof. destruct M as [??? []]; naive_solver. Qed.
 
   Lemma always_modality_emp : emp ⊢ M emp.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 9a9e4b145995bdaed64f6fe79f49226aa4164a69..4696f8422aca6be9dedde2f53fea42e0cfb36aaa 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -720,7 +720,8 @@ Proof.
       eauto using always_modality_spatial_transform.
   + rewrite -HQ' /= right_id comm -{2}(always_modality_spatial_clear M) //.
     by rewrite (True_intro ([∗] Γs)%I).
-  + by destruct (always_modality_spatial_id M).
+  + rewrite -HQ' {1}(always_modality_spatial_id M ([∗] Γs')%I) //.
+    by rewrite -always_modality_sep.
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :