From 06219a26579be30e2e21d767c29213af72aba342 Mon Sep 17 00:00:00 2001
From: HaleOIC <yunsongyang730@gmail.com>
Date: Wed, 8 Apr 2026 15:59:33 +0200
Subject: [PATCH 1/7] feat: clean up

---
 PORTING.md                                    |  16 +-
 src/Iris/BI/Updates.lean                      | 183 +++++++--
 src/Iris/Examples/Proofs.lean                 |   2 +-
 src/Iris/ProofMode/InstancesUpdates.lean      | 142 +++++--
 src/Iris/ProofMode/ModalityInstances.lean     |  34 +-
 src/Iris/ProofMode/Patterns/CasesPattern.lean |  12 +-
 src/Iris/ProofMode/Tactics/Cases.lean         | 252 ++++++------
 src/Iris/ProofMode/Tactics/Have.lean          |   3 +-
 src/Iris/ProofMode/Tactics/Intro.lean         |   8 +-
 src/Iris/Tests/Tactics.lean                   | 370 +++++++++++++-----
 tactics.md                                    |  16 +-
 11 files changed, 717 insertions(+), 321 deletions(-)

diff --git a/PORTING.md b/PORTING.md
index 632589a3..4152a787 100644
--- a/PORTING.md
+++ b/PORTING.md
@@ -237,8 +237,11 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
 - [ ] `sbi_unfold.v`
 - [ ] `telescopes.v`
 - [ ] `updates.v`
-  - [x] FUpd class
-  - [ ] Big op lemmas
+  - [x] Bupd laws 
+  - [x] Fupd basic laws 
+  - [ ] Fupd mask change laws
+  - [ ] Fupd step derived rules 
+  - [ ] Fupd plainly general laws
 - [ ] `weakestpre.v`
 - [ ] `lib/atomic.v`
 - [ ] `lib/core.v`
@@ -261,6 +264,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] instances for big ops
   - [ ] MaybeCombineSepAs instances
   - [ ] CombineSepGives instances
+  - [x] FromModal instances
   - [x] ElimModal instances
   - [ ] AddModal instances
   - [ ] ElimInv instances
@@ -294,11 +298,11 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] IntoLaterN
 - [ ] `class_instances_updates.v` (InstancesUpdates.lean)
   - [x] Basic instances for bupd
-  - [ ] Basic instances for fupd
+  - [x] Basic instances for fupd
   - [x] FromModal bupd
-  - [ ] FromModal fupd
+  - [x] FromModal fupd
   - [x] ElimModal bupd
-  - [ ] ElimModal fupd
+  - [x] ElimModal fupd
   - [ ] AddModal bupd
   - [ ] AddModal fupd
   - [ ] ElimAcc bupd
@@ -434,6 +438,8 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [ ] IClearFrame
 - [ ] `modalities.v`
 - [ ] `modality_instances.v`
+  - [ ] modality_embed 
+  - [x] others
 - [ ] `monpred.v`
 - [x] `proofmode.v` (ProofMode.lean)
 - [-] `reduction.v` (not necessary in Lean)
diff --git a/src/Iris/BI/Updates.lean b/src/Iris/BI/Updates.lean
index 8c9d328a..d8f9a0ea 100644
--- a/src/Iris/BI/Updates.lean
+++ b/src/Iris/BI/Updates.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Markus de Medeiros, Remy Seassau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus de Medeiros, Remy Seassau
+Authors: Markus de Medeiros, Remy Seassau, Yunsong Yang
 -/
 module
 
@@ -38,29 +38,46 @@ class FUpd (PROP : Type _) where
   fupd : CoPset → CoPset → PROP → PROP
 export FUpd (fupd)
 
-syntax "|={ " term " , " term " }=> " term : term
-syntax term "={ " term " , " term " }=∗ " term : term
-syntax "|={ " term " }=> " term : term
-syntax term "={ " term " }=∗ " term : term
+syntax "|={" term "," term "}=> " term : term
+syntax term "={" term "," term "}=∗ " term : term
+syntax "|={" term "}=> " term : term
+syntax term "={" term "}=∗ " term : term
 
 macro_rules
-  | `(iprop(|={ $E1 , $E2 }=> $P))  => ``(FUpd.fupd $E1 $E2 iprop($P))
-  | `(iprop($P ={ $E1 , $E2 }=∗ $Q))  => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E2 iprop($Q)))
-  | `(iprop(|={ $E1 }=> $P))  => ``(FUpd.fupd $E1 $E1 iprop($P))
-  | `(iprop($P ={ $E1 }=∗ $Q))  => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E1 iprop($Q)))
+  | `(iprop(|={$E1,$E2}=> $P))  => ``(FUpd.fupd $E1 $E2 iprop($P))
+  | `(iprop($P ={$E1,$E2}=∗ $Q))  => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E2 iprop($Q)))
+  | `(iprop(|={$E1}=> $P))  => ``(FUpd.fupd $E1 $E1 iprop($P))
+  | `(iprop($P ={$E1}=∗ $Q))  => ``(BIBase.wand iprop($P) (FUpd.fupd $E1 $E1 iprop($Q)))
+
+delab_rule FUpd.fupd
+  | `($_ $E1 $E2 $P) => do
+      let P ← Iris.BI.unpackIprop P
+      if E1 == E2 then ``(iprop(|={$E1}=> $P))
+      else ``(iprop(|={$E1,$E2}=> $P))
+
+syntax "|={" term "}[" term "]▷=> " term : term
+syntax term "={" term "}[" term "]▷=∗ " term : term
+syntax "|={" term "}▷=> " term : term
+syntax term "={" term "}▷=∗ " term : term
+
+macro_rules
+  | `(iprop(|={$E1}[$E2]▷=> $P))  => ``(iprop(|={$E1,$E2}=> ▷ (|={$E2,$E1}=> iprop($P))))
+  | `(iprop($P ={$E1}[$E2]▷=∗ $Q))  => ``(iprop(iprop($P) -∗ |={$E1}[$E2]▷=> iprop($Q)))
+  | `(iprop(|={$E1}▷=> $P))  => ``(iprop(|={$E1}[$E1]▷=> iprop($P)))
+  | `(iprop($P ={$E1}▷=∗ $Q))  => ``(iprop(iprop($P) ={$E1}[$E1]▷=∗ iprop($Q)))
 
 -- Delab rules
 
-syntax "|={ " term " }[ " term " ]▷=> " term : term
-syntax term "={ " term " }[ " term " ]▷=∗ " term : term
-syntax "|={ " term " }▷=> " term : term
-syntax term "={ " term " }▷=∗ " term : term
+syntax "|={" term "}[" term "]▷^" term "=> " term : term
+syntax term "={" term "}[" term "]▷^" term "=∗ " term : term
+syntax "|={" term "}▷^" term "=> " term : term
+syntax term "={" term "}▷^" term "=∗ " term : term
 
 macro_rules
-  | `(iprop(|={ $E1 }[ $E2 ]▷=> $P))  => ``(iprop(|={$E1, $E2}=> ▷ (|={ $E2, $E1 }=> iprop($P))))
-  | `(iprop($P ={ $E1 }[ $E2 ]▷=∗ $Q))  => ``(iprop(iprop($P) -∗ |={$E1}[$E2]▷=> iprop($Q)))
-  | `(iprop(|={ $E1 }▷=> $P))  => ``(iprop(|={$E1}[$E1]▷=> iprop($P)))
-  | `(iprop($P ={ $E1 }▷=∗ $Q))  => ``(iprop(iprop($P) ={$E1}[$E1]▷=∗ iprop($Q)))
+  | `(iprop(|={$E1}[$E2]▷^$n=> $P))  => ``(iprop(|={$E1,$E2}=> ▷^[$n] (|={$E2,$E1}=> iprop($P))))
+  | `(iprop($P ={$E1}[$E2]▷^$n=∗ $Q))  => ``(iprop(iprop($P) -∗ |={$E1}[$E2]▷^$n=> iprop($Q)))
+  | `(iprop(|={$E1}▷^$n=> $P))  => ``(iprop(|={$E1}[$E1]▷^$n=> iprop($P)))
+  | `(iprop($P ={$E1}▷^$n=∗ $Q))  => ``(iprop(iprop($P) ={$E1}[$E1]▷^$n=∗ iprop($Q)))
 
 -- Delab rules
 
@@ -79,26 +96,26 @@ macro_rules
 
 class BIUpdate (PROP : Type _) [BI PROP] extends BUpd PROP where
   [bupd_ne : OFE.NonExpansive (BUpd.bupd (PROP := PROP))]
-  intro {P : PROP} : iprop(P ⊢ |==> P)
-  mono {P Q : PROP} : iprop(P ⊢ Q) → iprop(|==> P ⊢ |==> Q)
-  trans {P : PROP} : iprop(|==> |==> P ⊢ |==> P)
-  frame_r {P R : PROP} : iprop((|==> P) ∗ R ⊢ |==> (P ∗ R))
+  intro {P : PROP} : P ⊢ |==> P
+  mono {P Q : PROP} : (P ⊢ Q) → |==> P ⊢ |==> Q
+  trans {P : PROP} : |==> |==> P ⊢ |==> P
+  frame_r {P R : PROP} : (|==> P) ∗ R ⊢ |==> (P ∗ R)
 
 class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
   [ne {E1 E2 : CoPset} : OFE.NonExpansive (FUpd.fupd E1 E2 (PROP := PROP))]
-  subset {E1 E2 : CoPset} : Subset E2 E1 → ⊢ |={E1, E2}=> |={E2, E1}=> (emp : PROP)
-  except0 {E1 E2 : CoPset} (P : PROP) : (◇ |={E1, E2}=> P) ⊢ |={E1, E2}=> P
-  trans {E1 E2 E3 : CoPset} (P : PROP) : (|={E1, E2}=> |={E2, E3}=> P) ⊢ |={E1, E3}=> P
-  mask_frame_r' {E1 E2 Ef : CoPset} (P : PROP) :
-    E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={CoPset.union E1 Ef, CoPset.union E2 Ef}=> P
-  frame_r {E1 E2 : CoPset} (P R : PROP) :
-    iprop((|={E1, E2}=> P) ∗ R ⊢ |={E1, E2}=> P ∗ R)
+  subset {E1 E2 : CoPset} : E2 ⊆ E1 → ⊢ |={E1,E2}=> |={E2,E1}=> (emp : PROP)
+  except0 {E1 E2 : CoPset} {P : PROP} : (◇ |={E1,E2}=> P) ⊢ |={E1,E2}=> P
+  mono {E1 E2 : CoPset} {P Q : PROP} : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q
+  trans {E1 E2 E3 : CoPset} {P : PROP} : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P
+  mask_frame_r' {E1 E2 Ef : CoPset} {P : PROP} :
+    E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P
+  frame_r {E1 E2 : CoPset} {P R : PROP} : (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R
 
 class BIUpdateFUpdate (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] where
-  fupd_of_bupd {P : PROP} {E : CoPset} : iprop(⊢ |==> P) → iprop(⊢ |={E}=> P)
+  fupd_of_bupd {P : PROP} {E : CoPset} : (|==> P) ⊢ |={E}=> P
 
 class BIBUpdatePlainly (PROP : Type _) [BI PROP] [BIUpdate PROP] [Sbi PROP] where
-  bupd_plainly {P : PROP} : iprop((|==> ■ P)) ⊢ P
+  bupd_plainly {P : PROP} : (|==> ■ P) ⊢ P
 
 class BIFUpdatePlainly (PROP : Type _) [BI PROP] [BIFUpdate PROP] [Sbi PROP] where
   fupd_plainly_keep_l (E E' : CoPset) (P R : PROP) : (R ={E,E'}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R
@@ -112,38 +129,38 @@ variable [BI PROP] [BIUpdate PROP]
 
 open BIUpdate
 
-theorem bupd_frame_l {P Q : PROP} : iprop(P ∗ |==> Q ⊢ |==> (P ∗ Q)) :=
+theorem bupd_frame_l {P Q : PROP} : P ∗ |==> Q ⊢ |==> (P ∗ Q) :=
   sep_symm.trans <| frame_r.trans <| mono sep_symm
 
-theorem bupd_frame_r {P Q : PROP} : iprop(|==> P ∗ Q ⊢ |==> (P ∗ Q)) :=
+theorem bupd_frame_r {P Q : PROP} : |==> P ∗ Q ⊢ |==> (P ∗ Q) :=
   frame_r
 
-theorem bupd_wand_l {P Q : PROP} : iprop((P -∗ Q) ∗ (|==> P) ⊢ |==> Q) :=
+theorem bupd_wand_l {P Q : PROP} : (P -∗ Q) ∗ (|==> P) ⊢ |==> Q :=
   bupd_frame_l.trans <| mono <| wand_elim .rfl
 
-theorem bupd_wand_r {P Q : PROP} : iprop((|==> P) ∗ (P -∗ Q) ⊢ |==> Q) :=
+theorem bupd_wand_r {P Q : PROP} : (|==> P) ∗ (P -∗ Q) ⊢ |==> Q :=
   sep_symm.trans bupd_wand_l
 
-theorem bupd_sep {P Q : PROP} : iprop((|==> P) ∗ (|==> Q) ⊢ |==> (P ∗ Q)) :=
+theorem bupd_sep {P Q : PROP} : (|==> P) ∗ (|==> Q) ⊢ |==> (P ∗ Q) :=
   bupd_frame_l.trans <| (mono <| frame_r).trans BIUpdate.trans
 
-theorem bupd_idem {P : PROP} : iprop((|==> |==> P) ⊣⊢ |==> P) :=
+theorem bupd_idem {P : PROP} : (|==> |==> P) ⊣⊢ |==> P :=
   ⟨BIUpdate.trans, BIUpdate.intro⟩
 
-theorem bupd_or {P Q: PROP} : iprop((|==> P) ∨ (|==> Q) ⊢ |==> (P ∨ Q)) :=
+theorem bupd_or {P Q: PROP} : (|==> P) ∨ (|==> Q) ⊢ |==> (P ∨ Q) :=
   or_elim (mono or_intro_l) (mono or_intro_r)
 
-theorem bupd_and {P Q : PROP} : iprop((|==> (P ∧ Q)) ⊢ (|==> P) ∧ (|==> Q)) :=
+theorem bupd_and {P Q : PROP} : (|==> (P ∧ Q)) ⊢ (|==> P) ∧ (|==> Q) :=
   and_intro (mono and_elim_l) (mono and_elim_r)
 
 theorem bupd_exist {Φ : A → PROP} : (∃ x : A, |==> Φ x) ⊢ |==> ∃ x : A, Φ x :=
   exists_elim (mono <| exists_intro ·)
 
 theorem bupd_forall {Φ : A → PROP} :
-    iprop(|==> «forall» fun x : A => Φ x) ⊢ «forall» fun x : A => iprop(|==> Φ x) :=
+    (|==> «forall» fun x : A => Φ x) ⊢ «forall» fun x : A => iprop(|==> Φ x) :=
   forall_intro (mono <| forall_elim ·)
 
-theorem bupd_except0 {P : PROP} : iprop(◇ (|==> P) ⊢ (|==> ◇ P)) :=
+theorem bupd_except0 {P : PROP} : ◇ (|==> P) ⊢ (|==> ◇ P) :=
   or_elim (or_intro_l.trans intro) (mono or_intro_r)
 
 instance {P : PROP} [Absorbing P] : Absorbing iprop(|==> P) :=
@@ -170,3 +187,89 @@ instance {P : PROP} [Plain P] : Plain iprop(|==> P) :=
   ⟨(mono Plain.plain).trans <| (bupd_elim).trans <| plainly_mono intro⟩
 
 end BUpdPlainlyLaws
+
+section FUpdLaws
+
+variable [BI PROP] [BIFUpdate PROP]
+
+open BIFUpdate
+
+theorem fupd_mask_intro_subseteq {E1 E2 : CoPset} {P : PROP} : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P :=
+  λ h => (emp_sep.2.trans <| sep_mono_l <| subset h).trans <|
+    frame_r.trans <| mono <| frame_r.trans <| mono emp_sep.1
+
+theorem fupd_intro {E : CoPset} {P : PROP} : P ⊢ |={E}=> P :=
+  (fupd_mask_intro_subseteq λ _ => id).trans trans
+
+-- Introduction lemma for a mask-chaging fupd
+theorem fupd_mask_intro {E1 E2 : CoPset} {P : PROP} :
+    E2 ⊆ E1 → ((|={E2,E1}=> emp) -∗ P) ⊢ |={E1,E2}=> P :=
+  λ h => (wand_mono_r fupd_intro).trans <|
+    (emp_sep.2.trans <| sep_mono_l <| subset h).trans <|
+    frame_r.trans <| (mono wand_elim_r).trans trans
+
+theorem fupd_mask_intro_discard {E1 E2 : CoPset} {P : PROP} [Absorbing P] : E2 ⊆ E1 → P ⊢ |={E1,E2}=> P :=
+  λ h => (wand_intro' sep_elim_r).trans <| fupd_mask_intro h
+
+theorem fupd_elim {E1 E2 E3 : CoPset} {P Q : PROP} : (Q ⊢ |={E2,E3}=> P) → (|={E1,E2}=> Q) ⊢ |={E1,E3}=> P :=
+  λ h => (mono h).trans trans
+
+theorem fupd_frame_l {E1 E2 : CoPset} {P Q : PROP} : P ∗ (|={E1,E2}=> Q) ⊢ |={E1,E2}=> P ∗ Q :=
+  sep_symm.trans <| frame_r.trans <| mono sep_symm
+
+theorem fupd_frame_r {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P) ∗ Q ⊢ |={E1,E2}=> P ∗ Q :=
+  frame_r
+
+theorem fupd_wand_l {E1 E2 : CoPset} {P Q : PROP} : (P -∗ Q) ∗ (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q :=
+  fupd_frame_l.trans <| mono <| wand_elim .rfl
+
+theorem fupd_wand_r {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P) ∗ (P -∗ Q) ⊢ |={E1,E2}=> Q :=
+  sep_symm.trans fupd_wand_l
+
+theorem fupd_sep {E : CoPset} {P Q : PROP} : (|={E}=> P) ∗ (|={E}=> Q) ⊢ |={E}=> P ∗ Q :=
+  fupd_frame_l.trans <| (mono frame_r).trans trans
+
+theorem fupd_idem {E : CoPset} {P : PROP} : (|={E}=> |={E}=> P) ⊣⊢ |={E}=> P := ⟨trans, fupd_intro⟩
+
+theorem fupd_or {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P) ∨ (|={E1,E2}=> Q) ⊢ |={E1,E2}=> P ∨ Q :=
+  or_elim (mono or_intro_l) (mono or_intro_r)
+
+theorem fupd_and {E1 E2 : CoPset} {P Q : PROP} : (|={E1,E2}=> P ∧ Q) ⊢ (|={E1,E2}=> P) ∧ (|={E1,E2}=> Q) :=
+  and_intro (mono and_elim_l) (mono and_elim_r)
+
+theorem fupd_exist {E1 E2 : CoPset} {Φ : A → PROP} : (∃ a : A, |={E1,E2}=> Φ a) ⊢ |={E1,E2}=> ∃ a : A, Φ a :=
+  exists_elim (mono <| exists_intro ·)
+
+theorem fupd_forall {E1 E2 : CoPset} {Φ : A → PROP} :
+    (|={E1,E2}=> «forall» λ a : A => Φ a) ⊢ «forall» λ a : A => iprop(|={E1,E2}=> Φ a) :=
+  forall_intro (mono <| forall_elim ·)
+
+theorem fupd_except0 {E1 E2 : CoPset} {P : PROP} : (◇ |={E1,E2}=> P) ⊢ |={E1,E2}=> ◇ P :=
+  except0.trans (mono except0_intro)
+
+instance {E1 E2 : CoPset} {P : PROP} [Absorbing P] : Absorbing iprop(|={E1,E2}=> P) :=
+  ⟨fupd_frame_l.trans <| mono sep_elim_r⟩
+
+theorem fupd_mask_frame_r {E1 E2 Ef : CoPset} {P : PROP} :
+    E1 ## Ef → (|={E1,E2}=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P :=
+  λ h => (mono <| imp_intro' and_elim_r).trans <| mask_frame_r' h
+
+-- TODO: the following theorems can be proved only with CoPSet extensional-equality
+-- theorem fupd_mask_frame {E E' E1 E2 : CoPset} {P : PROP} :
+--     E1 ⊆ E → (|={E1,E2}=> |={E2 ∪ (E \ E1),E'}=> P) ⊢ |={E,E'}=> P := sorry
+
+-- theorem fupd_mask_frame_acc {E E' E1 E2 : CoPset} {P Q : PROP}:
+--     E1 ⊆ E →
+--     (|={E1,E1 \ E2}=> Q) ⊢
+--     (Q -∗ |={E \ E2,E'}=> (∀ R, (|={E1 \ E2,E1}=> R) -∗ |={E \ E2,E}=> R) -∗  P) -∗
+--     (|={E,E'}=> P) := sorry
+
+-- theorem fupd_mask_mono {E1 E2 : CoPset} {P : PROP} :
+--     E1 ⊆ E2 → (|={E1}=> P) ⊢ |={E2}=> P := sorry
+
+-- theorem fupd_mask_subseteq_emptyset_difference {E1 E2 : CoPset} :
+--     E2 ⊆ E1 → ⊢ |={E1,E2}=> |={∅,E1\E2}=> (emp: PROP) := sorry
+
+-- theorem fupd_trans_frame {E1 E2 E3 : CoPset} {P Q : PROP} : ((Q ={E2,E3}=∗ emp) ∗ |={E1,E2}=> (Q ∗ P)) ⊢ |={E1,E3}=> P := sorry
+
+end FUpdLaws
diff --git a/src/Iris/Examples/Proofs.lean b/src/Iris/Examples/Proofs.lean
index cdada796..8675421f 100644
--- a/src/Iris/Examples/Proofs.lean
+++ b/src/Iris/Examples/Proofs.lean
@@ -16,7 +16,7 @@ open Iris.BI
 theorem proof_example_1 [BI PROP] (P Q R : PROP) (Φ : α → PROP) :
   P ∗ Q ∗ □ R ⊢ □ (R -∗ ∃ x, Φ x) -∗ ∃ x, Φ x ∗ P ∗ Q
 := by
-  iintro ⟨HP, HQ, □HR⟩ □HRΦ
+  iintro ⟨HP, HQ, #HR⟩ #HRΦ
   ihave HΦ := HRΦ $$ HR
   icases HΦ with ⟨%x, _HΦ⟩
   iexists x
diff --git a/src/Iris/ProofMode/InstancesUpdates.lean b/src/Iris/ProofMode/InstancesUpdates.lean
index 55be6f10..588db221 100644
--- a/src/Iris/ProofMode/InstancesUpdates.lean
+++ b/src/Iris/ProofMode/InstancesUpdates.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler
+Authors: Michael Sammler, Yunsong Yang
 -/
 module
 
@@ -12,77 +12,175 @@ public import Iris.Std.TC
 @[expose] public section
 
 namespace Iris.ProofMode
+
 open Iris.BI Iris.Std
 
-variable {PROP} [BI PROP]
+section BIBasicUpdate
+
+variable {PROP} [BI PROP] [BIUpdate PROP]
 
-instance fromAssumption_bupd [BIUpdate PROP] p ioP (P Q : PROP)
+instance fromAssumption_bupd p ioP (P Q : PROP)
     [h : FromAssumption p ioP P Q] : FromAssumption p ioP P iprop(|==> Q) where
   from_assumption := h.1.trans BIUpdate.intro
 
-instance fromPure_bupd [BIUpdate PROP] (a : Bool) (P : PROP) (φ : Prop)
+instance fromPure_bupd (a : Bool) (P : PROP) (φ : Prop)
     [h : FromPure a P φ] : FromPure a iprop(|==> P) φ where
   from_pure := h.1.trans BIUpdate.intro
 
-instance intoWand_bupd [BIUpdate PROP] (p q : Bool) ioP ioQ (R P Q : PROP)
+instance intoWand_bupd (p q : Bool) ioP ioQ (R P Q : PROP)
     [h : IntoWand false false R ioP P ioQ Q] :
     IntoWand p q iprop(|==> R) ioP iprop(|==> P) ioQ iprop(|==> Q) where
   into_wand := intuitionisticallyIf_elim.trans <|
     wand_intro <| (sep_mono (BIUpdate.mono h.1) intuitionisticallyIf_elim).trans <|
     bupd_sep.trans <| BIUpdate.mono wand_elim_l
 
-instance intoWand_bupd_persistent [BIUpdate PROP] (p q : Bool) ioP ioQ (R P Q : PROP)
+instance intoWand_bupd_persistent (p q : Bool) ioP ioQ (R P Q : PROP)
     [h : IntoWand false q R ioP P ioQ Q] :
     IntoWand p q iprop(|==> R) ioP P ioQ iprop(|==> Q) where
   into_wand := intuitionisticallyIf_elim.trans <|
     wand_intro <| (sep_mono (BIUpdate.mono h.1) .rfl).trans <|
     bupd_frame_r.trans <| BIUpdate.mono wand_elim_l
 
-instance fromSep_bupd [BIUpdate PROP] (P Q1 Q2 : PROP)
+instance fromSep_bupd (P Q1 Q2 : PROP)
     [h : FromSep P Q1 Q2] : FromSep iprop(|==> P) iprop(|==> Q1) iprop(|==> Q2) where
   from_sep := bupd_sep.trans (BIUpdate.mono h.1)
 
-instance fromOr_bupd [BIUpdate PROP] (P Q1 Q2 : PROP)
+instance fromOr_bupd (P Q1 Q2 : PROP)
     [h : FromOr P Q1 Q2] : FromOr iprop(|==> P) iprop(|==> Q1) iprop(|==> Q2) where
   from_or := bupd_or.trans (BIUpdate.mono h.1)
 
-instance intoAnd_bupd [BIUpdate PROP] (P Q1 Q2 : PROP)
+instance intoAnd_bupd (P Q1 Q2 : PROP)
     [h : IntoAnd false P Q1 Q2] : IntoAnd false iprop(|==> P) iprop(|==> Q1) iprop(|==> Q2) where
   into_and := (BIUpdate.mono h.1).trans bupd_and
 
-instance fromExists_bupd [BIUpdate PROP] (P : PROP) (Φ : α → PROP)
+instance fromExists_bupd (P : PROP) (Φ : α → PROP)
     [h : FromExists P Φ] : FromExists iprop(|==> P) (fun a => iprop(|==> Φ a)) where
   from_exists := bupd_exist.trans (BIUpdate.mono h.1)
 
-instance intoForall_bupd [BIUpdate PROP] (P : PROP) (Φ : α → PROP)
+instance intoForall_bupd (P : PROP) (Φ : α → PROP)
     [h : IntoForall P Φ] : IntoForall iprop(|==> P) (fun a => iprop(|==> Φ a)) where
   into_forall := (BIUpdate.mono h.1).trans bupd_forall
 
-instance isExcept0_bupd [BIUpdate PROP] (P : PROP)
+instance isExcept0_bupd (P : PROP)
     [h : IsExcept0 P] : IsExcept0 iprop(|==> P) where
   is_except0 := bupd_except0.trans <| BIUpdate.mono h.1
 
-instance fromModal_bupd [BIUpdate PROP] (P : PROP) :
+instance fromModal_bupd (P : PROP) :
     FromModal True modality_id iprop(|==> P) iprop(|==> P) P where
   from_modal := by simp [modality_id]; exact BIUpdate.intro
 
-instance elimModal_bupd [BIUpdate PROP] p (P Q : PROP) :
-  ElimModal True p false iprop(|==> P) P iprop(|==> Q) iprop(|==> Q) where
-  elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans $ bupd_frame_r.trans $ (BIUpdate.mono wand_elim_r).trans BIUpdate.trans
+instance elimModal_bupd p (P Q : PROP) :
+    ElimModal True p false iprop(|==> P) P iprop(|==> Q) iprop(|==> Q) where
+  elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans <|
+    bupd_frame_r.trans <| (BIUpdate.mono wand_elim_r).trans BIUpdate.trans
 
-end Iris.ProofMode
+end BIBasicUpdate
 
-namespace Iris.ProofMode
-open Iris.BI Iris.Std
+section SBIBasicUpdate
 
 variable {PROP} [Sbi PROP] [BIUpdate PROP] [BIBUpdatePlainly PROP]
 
 @[ipm_backtrack]
 instance elimModal_bupd_plain_goal p (P Q : PROP) [Plain Q] :
-  ElimModal True p false iprop(|==> P) P Q Q where
-  elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans $ bupd_frame_r.trans $ (BIUpdate.mono wand_elim_r).trans bupd_elim
+    ElimModal True p false iprop(|==> P) P Q Q where
+  elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans <|
+    bupd_frame_r.trans <| (BIUpdate.mono wand_elim_r).trans bupd_elim
 
 @[ipm_backtrack]
 instance elimModal_bupd_plain p (P Q : PROP) [Plain P] :
-  ElimModal True p p iprop(|==> P) P Q Q where
+    ElimModal True p p iprop(|==> P) P Q Q where
   elim_modal _ := (sep_mono_l (intuitionisticallyIf_mono bupd_elim)).trans wand_elim_r
+
+end SBIBasicUpdate
+
+section BIFancyUpdate
+
+variable {PROP} [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+
+instance fromAssumption_fupd E p ioP (P Q : PROP)
+    [h : FromAssumption p ioP P iprop(|==> Q)] : FromAssumption p ioP P iprop(|={E}=> Q) where
+  from_assumption := h.from_assumption.trans BIUpdateFUpdate.fupd_of_bupd
+
+instance fromPure_fupd E a (P : PROP) (φ : Prop)
+    [h : FromPure a P φ] : FromPure a iprop(|={E}=> P) φ where
+  from_pure := h.from_pure.trans <| fupd_intro
+
+instance intoWand_fupd E (p q : Bool) ioP ioQ (R P Q : PROP)
+    [h : IntoWand false false R ioP P ioQ Q] :
+    IntoWand p q iprop(|={E}=> R) ioP iprop(|={E}=> P) ioQ iprop(|={E}=> Q) where
+  into_wand := intuitionisticallyIf_elim.trans <|
+    wand_intro <| (sep_mono (BIFUpdate.mono h.into_wand) intuitionisticallyIf_elim).trans <|
+    fupd_sep.trans <| BIFUpdate.mono wand_elim_l
+
+instance intoWand_fupd_persistent E1 E2 (p q : Bool) ioP ioQ (R P Q : PROP)
+    [h : IntoWand false q R ioP P ioQ Q] :
+    IntoWand p q iprop(|={E1,E2}=> R) ioP P ioQ iprop(|={E1,E2}=> Q) where
+  into_wand := intuitionisticallyIf_elim.trans <|
+    wand_intro <| (sep_mono (BIFUpdate.mono h.into_wand) .rfl).trans <|
+    fupd_frame_r.trans <| BIFUpdate.mono wand_elim_l
+
+instance fromSep_fupd E (P Q1 Q2 : PROP)
+    [h : FromSep P Q1 Q2] : FromSep iprop(|={E}=> P) iprop(|={E}=> Q1) iprop(|={E}=> Q2) where
+  from_sep := fupd_sep.trans <| BIFUpdate.mono h.from_sep
+
+instance fromOr_fupd E1 E2 (P Q1 Q2 : PROP)
+    [h : FromOr P Q1 Q2] : FromOr iprop(|={E1,E2}=> P) iprop(|={E1,E2}=> Q1) iprop(|={E1,E2}=> Q2) where
+  from_or := fupd_or.trans <| BIFUpdate.mono h.from_or
+
+instance intoAnd_fupd E1 E2 (P Q1 Q2 : PROP)
+    [h : IntoAnd false P Q1 Q2] : IntoAnd false iprop(|={E1,E2}=> P) iprop(|={E1,E2}=> Q1) iprop(|={E1,E2}=> Q2) where
+  into_and := (BIFUpdate.mono h.into_and).trans fupd_and
+
+instance fromExists_fupd E1 E2 (P : PROP) (Φ : α → PROP)
+    [h : FromExists P Φ] : FromExists iprop(|={E1,E2}=> P) (fun a => iprop(|={E1,E2}=> Φ a)) where
+  from_exists := fupd_exist.trans <| (BIFUpdate.mono h.from_exists)
+
+instance intoForall_fupd E1 E2 (P : PROP) (Φ : α → PROP)
+    [h : IntoForall P Φ] : IntoForall iprop(|={E1,E2}=> P) (fun a => iprop(|={E1,E2}=> Φ a)) where
+  into_forall := (BIFUpdate.mono h.into_forall).trans fupd_forall
+
+instance isExcept0_fupd E1 E2 (P : PROP) : IsExcept0 iprop(|={E1,E2}=> P) where
+  is_except0 := BIFUpdate.except0
+
+instance fromModal_fupd E (P : PROP) :
+    FromModal True modality_id iprop(|={E}=> P) iprop(|={E}=> P) P where
+  from_modal := by simp [modality_id]; exact fupd_intro
+
+instance elimModal_bupd_fupd p E1 E2 (P Q : PROP) :
+    ElimModal True p false iprop(|==> P) P iprop(|={E1,E2}=> Q) iprop(|={E1,E2}=> Q) where
+  elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans <|
+    (sep_mono_l BIUpdateFUpdate.fupd_of_bupd).trans <|
+    fupd_frame_r.trans <| (BIFUpdate.mono wand_elim_r).trans BIFUpdate.trans
+
+instance (priority := high) elimModal_fupd_fupd p E1 E2 E3 (P Q : PROP) :
+    ElimModal True p false iprop(|={E1,E2}=> P) P iprop(|={E1,E3}=> Q) iprop(|={E2,E3}=> Q) where
+  elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans <|
+    fupd_frame_r.trans <| (BIFUpdate.mono wand_elim_r).trans BIFUpdate.trans
+
+end BIFancyUpdate
+
+section SBIFancyUpdate
+
+variable {PROP} [Sbi PROP] [BIFUpdate PROP] [BIFUpdatePlainly PROP] [BIAffine PROP]
+
+-- instance fromForall_fupd E1 E2 (P : PROP) (Φ : α → PROP)
+--     [h : FromForall P Φ] [∀ a, Plain (Φ a)] :
+--     FromForall iprop(|={E1,E2}=> P) (fun a => iprop(|={E1,E2}=> Φ a)) where
+--   from_forall := sorry
+
+-- instance fromForall_stepFupd E (P : PROP) (Φ : α → PROP)
+--     [h : FromForall P Φ] [∀ a, Plain (Φ a)] :
+--     FromForall iprop(|={E}▷=> P) (fun a => iprop(|={E}▷=> Φ a)) where
+--   from_forall := sorry
+
+-- @[ipm_backtrack]
+-- instance elimModal_fupd_plain_goal p E (P Q : PROP) [Plain Q] :
+--     ElimModal True p false iprop(|={E}=> P) P Q Q where
+--   elim_modal _ := sorry
+
+-- @[ipm_backtrack]
+-- instance elimModal_fupd_plain p E (P Q : PROP) [Plain P] :
+--     ElimModal True p p iprop(|={E}=> P) P Q Q where
+--   elim_modal _ := sorry
+
+end SBIFancyUpdate
diff --git a/src/Iris/ProofMode/ModalityInstances.lean b/src/Iris/ProofMode/ModalityInstances.lean
index 7f1c35a2..479686af 100644
--- a/src/Iris/ProofMode/ModalityInstances.lean
+++ b/src/Iris/ProofMode/ModalityInstances.lean
@@ -5,9 +5,6 @@ Authors: Markus de Medeiros, Michael Sammler
 -/
 module
 
-public import Iris.BI
-public import Iris.BI.DerivedLaws
-public import Iris.ProofMode.Modalities
 public import Iris.ProofMode.Classes
 
 @[expose] public section
@@ -17,9 +14,7 @@ open Iris.BI
 
 section Modalities
 
-variable [BI PROP]
-
-def modality_persistently : Modality PROP PROP where
+def modality_persistently [BI PROP] : Modality PROP PROP where
   M := persistently
   action
   | true => .id
@@ -31,10 +26,7 @@ def modality_persistently : Modality PROP PROP where
   mono := (persistently_mono ·)
   sep := persistently_sep_2
 
-unif_hint [BIBase PROP] (P : PROP) where |- iprop(□?false P) ≟ iprop(P)
-unif_hint [BIBase PROP] (P : PROP) where |- iprop(□?true P) ≟ iprop(□ P)
-
-def modality_affinely : Modality PROP PROP where
+def modality_affinely [BI PROP] : Modality PROP PROP where
   M := affinely
   action
   | true => .id
@@ -46,7 +38,7 @@ def modality_affinely : Modality PROP PROP where
   mono := (affinely_mono ·)
   sep := affinely_sep_2
 
-def modality_intuitionistically : Modality PROP PROP where
+def modality_intuitionistically [BI PROP] : Modality PROP PROP where
   M := intuitionistically
   action
   | true => .id
@@ -58,16 +50,6 @@ def modality_intuitionistically : Modality PROP PROP where
   mono := (intuitionistically_mono ·)
   sep := intuitionistically_sep_2
 
-def modality_laterN (n : Nat) : Modality PROP PROP where
-  M := BIBase.laterN n
-  action := λ _ => .transform (IntoLaterN false n)
-  spec := λ _ _ _ h => (intuitionisticallyIf_mono (h.1)).trans (laterN_intuitionisticallyIf_2 n)
-  emp := laterN_intro n
-  mono := (laterN_mono n ·)
-  sep := (laterN_sep n).2
-
-end Modalities
-
 def modality_plainly [Sbi PROP] : Modality PROP PROP where
   M := BIBase.Plainly.plainly
   action
@@ -79,3 +61,13 @@ def modality_plainly [Sbi PROP] : Modality PROP PROP where
   emp := plainly_emp_2
   mono := (plainly_mono ·)
   sep := plainly_sep_2
+
+def modality_laterN (n : Nat) [BI PROP] : Modality PROP PROP where
+  M := BIBase.laterN n
+  action := λ _ => .transform (IntoLaterN false n)
+  spec := λ _ _ _ h => (intuitionisticallyIf_mono (h.1)).trans (laterN_intuitionisticallyIf_2 n)
+  emp := laterN_intro n
+  mono := (laterN_mono n ·)
+  sep := (laterN_sep n).2
+
+end Modalities
diff --git a/src/Iris/ProofMode/Patterns/CasesPattern.lean b/src/Iris/ProofMode/Patterns/CasesPattern.lean
index 77d3b0f2..b321567d 100644
--- a/src/Iris/ProofMode/Patterns/CasesPattern.lean
+++ b/src/Iris/ProofMode/Patterns/CasesPattern.lean
@@ -18,15 +18,11 @@ syntax binderIdent : icasesPat
 syntax "-" : icasesPat
 syntax "⟨" icasesPatAlts,* "⟩" : icasesPat
 syntax "(" icasesPatAlts ")" : icasesPat
-syntax "⌜" binderIdent "⌝" : icasesPat
-syntax "□" icasesPat : icasesPat
+syntax "%" binderIdent : icasesPat
+syntax "#" icasesPat : icasesPat
 syntax "∗" icasesPat : icasesPat
 syntax ">" icasesPat : icasesPat
 
-macro "%" pat:binderIdent : icasesPat => `(icasesPat| ⌜$pat⌝)
-macro "#" pat:icasesPat : icasesPat => `(icasesPat| □ $pat)
-macro "*" pat:icasesPat : icasesPat => `(icasesPat| ∗ $pat)
-
 -- TODO: attach syntax to iCasesPat such that one can use withRef to
 -- associate the errors with the right part of the syntax
 inductive iCasesPat
@@ -49,8 +45,8 @@ where
   | `(icasesPat| $name:binderIdent) => some <| .one name
   | `(icasesPat| -) => some <| .clear
   | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ·.toList)
-  | `(icasesPat| ⌜$pat⌝) => some <| .pure pat
-  | `(icasesPat| □$pat) => go pat |>.map .intuitionistic
+  | `(icasesPat| %$pat:binderIdent) => some <| .pure pat
+  | `(icasesPat| #$pat) => go pat |>.map .intuitionistic
   | `(icasesPat| ∗$pat) => go pat |>.map .spatial
   | `(icasesPat| >$pat) => go pat |>.map .mod
   | `(icasesPat| ($pat)) => goAlts pat
diff --git a/src/Iris/ProofMode/Tactics/Cases.lean b/src/Iris/ProofMode/Tactics/Cases.lean
index 723d81f7..bd9362da 100644
--- a/src/Iris/ProofMode/Tactics/Cases.lean
+++ b/src/Iris/ProofMode/Tactics/Cases.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König, Mario Carneiro, Michael Sammler
+Authors: Lars König, Mario Carneiro, Michael Sammler, Yunsong Yang
 -/
 module
 
@@ -63,175 +63,186 @@ public meta section
 open Lean Elab Tactic Meta Qq Std
 
 private def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop))
-    {P} (_hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool))
-    (_k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q)) :
-    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
-  if let .defEq _ ← isDefEqQ A' q(iprop(False)) then
+    {P} (_hyps : Hyps bi P) (p : Q(Bool)) (A goal : Q($prop)) :
+    ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
+  if let .defEq _ ← isDefEqQ A q(iprop(False)) then
     return q(false_elim')
   else
-    throwError "icases: cannot destruct {A'} as an empty conjunct"
+    throwError "icases: cannot destruct {A} as an empty conjunct"
 
-private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
-    (name : TSyntax ``binderIdent)
-    (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) :
-    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
+/-- Destruct an existential hypothesis [A] by introducing its witness and continuing with the body [B]. -/
+private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (name : TSyntax ``binderIdent)
+    (p : Q(Bool)) (P A goal : Q($prop))
+    (k : (B : Q($prop)) → ProofModeM Q($P ∗ □?$p $B ⊢ $goal)) :
+    ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
   let v ← mkFreshLevelMVar
-  let α : Quoted q(Sort v) ← mkFreshExprMVarQ q(Sort v)
-  let Φ : Quoted q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
-  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoExists $A' $Φ)
-    | throwError "icases: {A'} is not an existential quantifier"
+  let α : Q(Sort v) ← mkFreshExprMVarQ q(Sort v)
+  let Φ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
+  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoExists $A $Φ)
+    | throwError "icases: {A} is not an existential quantifier"
   let (name, ref) ← getFreshName name
   withLocalDeclDQ name α fun x => do
     addLocalVarInfo ref (← getLCtx) x α
-    have B' : Q($prop) := Expr.headBeta q($Φ $x)
-    have : $B' =Q $Φ $x := ⟨⟩
-    have ⟨B, _⟩ := mkIntuitionisticIf bi p B'
-    let pf : Q(∀ x, $P ∗ □?$p $Φ x ⊢ $Q) ← mkLambdaFVars #[x] <|← k B B' ⟨⟩
-    return q(exists_elim' (A := $A') $pf)
-
-private def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (right : Bool)
-  (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) :
-    ProofModeM (Option Q($P ∗ □?$p $A' ⊢ $Q)) := do
+    have B : Q($prop) := Expr.headBeta q($Φ $x)
+    let pf : Q(∀ x, $P ∗ □?$p $Φ x ⊢ $goal) ← mkLambdaFVars #[x] <|← k B
+    return q(exists_elim' $pf)
+
+/-- Destruct a conjunction hypothesis [A] and continue with only its left or right component. -/
+private def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop))
+    (p : Q(Bool)) (P A goal : Q($prop)) (right : Bool)
+    (k : (B : Q($prop)) → ProofModeM Q($P ∗ □?$p $B ⊢ $goal)) :
+    ProofModeM (Option Q($P ∗ □?$p $A ⊢ $goal)) := do
   let A1 ← mkFreshExprMVarQ q($prop)
   let A2 ← mkFreshExprMVarQ q($prop)
-  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoAnd $p $A' $A1 $A2)
+  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoAnd $p $A $A1 $A2)
     | return none
-  if right then
-    have ⟨A2', _⟩ := mkIntuitionisticIf bi p A2
-    return some q(sep_and_elim_r $(← k A2' A2 ⟨⟩))
-  else
-    have ⟨A1', _⟩ := mkIntuitionisticIf bi p A1
-    return some q(sep_and_elim_l $(← k A1' A1 ⟨⟩))
+  if right then return some q(sep_and_elim_r $(← k A2))
+  else return some q(sep_and_elim_l $(← k A1))
 
+/-- Destruct a conjunction hypothesis [A] into two parts and continue with the left and right subpatterns in sequence. -/
 private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop))
-    {P} (hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool))
-    (k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q))
-    (k1 k2 : ∀ {P}, Hyps bi P → (Q B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) →
-      (∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q)) → ProofModeM Q($P ∗ $B ⊢ $Q)) :
-    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
+    {P} (hyps : Hyps bi P) (p : Q(Bool)) (A goal : Q($prop))
+    (k : ∀ {P}, Hyps bi P → (goal : Q($prop)) → ProofModeM Q($P ⊢ $goal))
+    (k1 k2 : ∀ {P}, Hyps bi P → (goal B : Q($prop)) →
+      (∀ {P}, Hyps bi P → (goal : Q($prop)) → ProofModeM Q($P ⊢ $goal)) →
+      ProofModeM Q($P ∗ □?$p $B ⊢ $goal)) :
+    ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
   let A1 ← mkFreshExprMVarQ q($prop)
   let A2 ← mkFreshExprMVarQ q($prop)
   match matchBool p with
   | .inl _ =>
-    let .some _ ← ProofModeM.trySynthInstanceQ q(IntoAnd $p $A' $A1 $A2)
-      | throwError "icases: cannot destruct {A'}"
-    let Q' := q(iprop(□ $A2 -∗ $Q))
-    let pf ← k1 hyps Q' q(iprop(□ $A1)) A1 ⟨⟩ fun hyps => do
-      let pf ← k2 hyps Q q(iprop(□ $A2)) A2 ⟨⟩ k
-      return q(wand_intro $pf)
-    return q(and_elim_intuitionistic (A := $A') $pf)
+    let .some _ ← ProofModeM.trySynthInstanceQ q(IntoAnd $p $A $A1 $A2)
+      | throwError "icases: cannot destruct {A}"
+    let goal' := q(iprop(□ $A2 -∗ $goal))
+    let pf ← k1 hyps goal' A1 fun hyps goal' => do
+      let goal'' ← mkFreshExprMVarQ q($prop)
+      let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $goal' iprop(□ $A2) $goal'')
+        | throwError "icases: internal error: {goal'} is not a wand"
+      let pf ← k2 hyps goal'' A2 k
+      return q((wand_intro $pf).trans from_wand)
+    return q(and_elim_intuitionistic $pf)
   | .inr _ =>
-    let .some _ ← ProofModeM.trySynthInstanceQ q(IntoSep $A' $A1 $A2)
-      | throwError "icases: cannot destruct {A'}"
-    let Q' := q(iprop($A2 -∗ $Q))
-    let pf ← k1 hyps Q' A1 A1 ⟨⟩ fun hyps => do
-      let pf ← k2 hyps Q A2 A2 ⟨⟩ k
-      return q(wand_intro $pf)
-    return q(sep_elim_spatial (A := $A') $pf)
-
-private def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
-    (k1 k2 : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) :
-    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
+    let .some _ ← ProofModeM.trySynthInstanceQ q(IntoSep $A $A1 $A2)
+      | throwError "icases: cannot destruct {A}"
+    let goal' := q(iprop($A2 -∗ $goal))
+    let pf ← k1 hyps goal' A1 fun hyps goal' => do
+      let goal'' ← mkFreshExprMVarQ q($prop)
+      let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $goal' $A2 $goal'')
+        | throwError "icases: internal error: {goal'} is not a wand"
+      let pf ← k2 hyps goal'' A2 k
+      return q((wand_intro $pf).trans from_wand)
+    return q(sep_elim_spatial (A := $A) $pf)
+
+/-- Destruct a disjunction hypothesis [A] into two cases and continue separately on each branch. -/
+private def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop))
+    (p : Q(Bool)) (P A goal : Q($prop))
+    (k1 k2 : (B : Q($prop)) → ProofModeM Q($P ∗ □?$p $B ⊢ $goal)) :
+    ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
   let A1 ← mkFreshExprMVarQ q($prop)
   let A2 ← mkFreshExprMVarQ q($prop)
-  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoOr $A' $A1 $A2)
-    | throwError "icases: {A'} is not a disjunction"
-  have ⟨A1', _⟩ := mkIntuitionisticIf bi p A1
-  have ⟨A2', _⟩ := mkIntuitionisticIf bi p A2
-  let pf1 ← k1 A1' A1 ⟨⟩
-  let pf2 ← k2 A2' A2 ⟨⟩
-  return q(or_elim' (A := $A') $pf1 $pf2)
-
-private def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
-    (k : (B' : Q($prop)) → ProofModeM Q($P ∗ □ $B' ⊢ $Q)) :
-    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
-  let B' ← mkFreshExprMVarQ q($prop)
-  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently $p $A' $B')
-    | throwError "icases: {A'} not persistent"
+  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoOr $A $A1 $A2)
+    | throwError "icases: {A} is not a disjunction"
+  return q(or_elim' $(← k1 A1) $(← k2 A2))
+
+/-- Destruct a persistent hypothesis [A] by turning it into an explicit [□ B] and continuing with the persistent body. -/
+private def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop))
+    (p : Q(Bool)) (P A goal : Q($prop))
+    (k : (B : Q($prop)) → ProofModeM Q($P ∗ □ $B ⊢ $goal)) :
+    ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
+  let B ← mkFreshExprMVarQ q($prop)
+  let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently $p $A $B)
+    | throwError "icases: {A} not persistent"
   match matchBool p with
   | .inl _ =>
-    return q(intuitionistic_elim_intuitionistic $(← k B'))
+    return q(intuitionistic_elim_intuitionistic $(← k B))
   | .inr _ =>
-    let .some _ ← trySynthInstanceQ q(TCOr (Affine $A') (Absorbing $Q))
-      | throwError "icases: {A'} not affine and the goal not absorbing"
-    return q(intuitionistic_elim_spatial (A := $A') $(← k B'))
-
-private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
-    (k : (B' : Q($prop)) → ProofModeM Q($P ∗ $B' ⊢ $Q)) :
-    ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
-  let B' ← mkFreshExprMVarQ q($prop)
+    let .some _ ← trySynthInstanceQ q(TCOr (Affine $A) (Absorbing $goal))
+      | throwError "icases: {A} not affine and the goal not absorbing"
+    return q(intuitionistic_elim_spatial (A := $A) $(← k B))
+
+/-- Destruct an affine/spatial hypothesis [A] by removing the affinely wrapper and continuing with the spatial body. -/
+private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop))
+    (p : Q(Bool)) (P A goal : Q($prop))
+    (k : (B : Q($prop)) → ProofModeM Q($P ∗ $B ⊢ $goal)) :
+    ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) := do
+  let B ← mkFreshExprMVarQ q($prop)
   -- this should always succeed
-  let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B' $A' $p)
-  return q(spatial_elim (A := $A') $(← k B'))
-
--- TODO: Why does this function require both A and A' instead of just A'?
-variable {u : Level} {prop : Q(Type u)} (bi : Q(BI $prop)) in
-partial def iCasesCore
-    {P} (hyps : Hyps bi P) (Q : Q($prop)) (p : Q(Bool))
-    (A A' : Q($prop)) (_ : $A =Q iprop(□?$p $A'))
-    (pat : iCasesPat) (k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q)) : ProofModeM (Q($P ∗ $A ⊢ $Q)) :=
+  let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A $p)
+  return q(spatial_elim $(← k B))
+
+variable {prop : Q(Type u)} (bi : Q(BI $prop)) in
+/--
+Recursively destruct the current hypothesis `□?p A` in the proof-mode context `hyps`
+according to the cases pattern `pat`. After the pattern has been processed, the
+continuation `k` is called with the updated context and, for modal patterns,
+possibly an updated goal.
+
+## Parameters
+- `hyps`: The current proof mode hypothesis context
+- `goal`: The current BI goal
+- `pat`: The cases pattern describing how to destruct the current hypothesis
+- `p`: Whether the current hypothesis is persistent
+- `A`: The payload proposition of the current hypothesis
+- `k`: The continuation representing the remaining proof after this destruct step
+
+## Returns
+A proof of `hyps ∗ □?p A ⊢ goal`.
+-/
+partial def iCasesCore {P} (hyps : Hyps bi P) (goal : Q($prop)) (pat : iCasesPat)
+    (p : Q(Bool)) (A : Q($prop))
+    (k : ∀ {P}, Hyps bi P → (goal' : Q($prop)) → ProofModeM Q($P ⊢ $goal)) :
+    ProofModeM (Q($P ∗ □?$p $A ⊢ $goal)) :=
   match pat with
   | .one name => do
     -- TODO: use Hyps.addWithInfo here?
     let (name, ref) ← getFreshName name
     let uniq ← mkFreshId
-    addHypInfo ref name uniq prop A' (isBinder := true)
-    let hyp := .mkHyp bi name uniq p A' A
-    if let .emp _ := hyps then
-      let pf : Q($A ⊢ $Q) ← k hyp
-      pure q(of_emp_sep $pf)
-    else
-      k (.mkSep hyps hyp)
+    addHypInfo ref name uniq prop A (isBinder := true)
+    let hyp := .mkHyp bi name uniq p A
+    if let .emp _ := hyps then pure q(of_emp_sep $(← k hyp goal))
+    else k (.mkSep hyps hyp) goal
 
   | .clear => do
-    let pf ← iClearCore bi q(iprop($P ∗ $A)) P p A' Q q(.rfl)
-    pure q($pf $(← k hyps))
+    let pf ← iClearCore bi q(iprop($P ∗ □?$p $A)) P p A goal q(.rfl)
+    pure q($pf $(← k hyps goal))
 
-  | .conjunction [arg] | .disjunction [arg] => iCasesCore hyps Q p A A' ⟨⟩ arg @k
+  | .conjunction [arg] | .disjunction [arg] => iCasesCore hyps goal arg p A @k
 
   | .disjunction [] => throwUnsupportedSyntax
 
-  | .conjunction [] => iCasesEmptyConj bi hyps Q A' p @k
+  | .conjunction [] => iCasesEmptyConj bi hyps p A goal
 
   -- pure conjunctions are always handled as existentials. There is
   -- intoExist_and_pure and intoExist_sep_pure to make this work as
   -- expected for pure assertions that are not explicit existentials.
   | .conjunction (.pure arg :: args) => do
-    iCasesExists bi P Q A' p arg
-      (iCasesCore hyps Q p · · · (.conjunction args) k)
+    iCasesExists bi arg p P A goal (iCasesCore hyps goal (.conjunction args) p · k)
   | .conjunction (arg :: args) => do
     if arg matches .clear then
-      let pf ← iCasesAndLR bi P Q A' p (right := true) fun B B' h =>
-        iCasesCore hyps Q p B B' h (.conjunction args) @k
-      if let some pf := pf then return pf
+      if let some pf ← iCasesAndLR bi p P A goal true λ B =>
+        iCasesCore hyps goal (.conjunction args) p B @k then return pf
     if args matches [.clear] then
-      let pf ← iCasesAndLR bi P Q A' p (right := false) fun B B' h =>
-        iCasesCore hyps Q p B B' h arg @k
-      if let some pf := pf then return pf
-    iCasesSep bi hyps Q A' p @k
-      (iCasesCore · · p · · · arg)
-      (iCasesCore · · p · · · (.conjunction args))
+      if let some pf ← iCasesAndLR bi p P A goal false λ B =>
+        iCasesCore hyps goal arg p B @k then return pf
+    iCasesSep bi hyps p A goal @k (iCasesCore · · arg p · ·)
+      (iCasesCore · · (.conjunction args) p · ·)
 
   | .disjunction (arg :: args) =>
-    iCasesOr bi P Q A' p
-      (iCasesCore hyps Q p · · · arg @k)
-      (iCasesCore hyps Q p · · · (.disjunction args) @k)
+    iCasesOr bi p P A goal (iCasesCore hyps goal arg p · k)
+      (iCasesCore hyps goal (.disjunction args) p · k)
 
   | .pure arg => do
-    iPureCore bi q(iprop($P ∗ $A)) P p A' Q arg q(.rfl) fun _ _ => k hyps
+    iPureCore bi q(iprop($P ∗ □?$p $A)) P p A goal arg q(.rfl) λ _ _ => k hyps goal
 
   | .intuitionistic arg =>
-    iCasesIntuitionistic bi P Q A' p fun B' =>
-      iCasesCore hyps Q q(true) q(iprop(□ $B')) B' ⟨⟩ arg @k
+    iCasesIntuitionistic bi p P A goal (iCasesCore hyps goal arg q(true) · @k)
 
   | .spatial arg =>
-    iCasesSpatial bi P Q A' p fun B' =>
-      iCasesCore hyps Q q(false) B' B' ⟨⟩ arg @k
+    iCasesSpatial bi p P A goal (iCasesCore hyps goal arg q(false) · @k)
 
   | .mod arg =>
-    iModCore bi P Q p A' fun p' A' Q' =>
-      have ⟨A'', eq⟩ := mkIntuitionisticIf bi p' A'
-      iCasesCore hyps Q' p' A'' A' eq arg @k
+    iModCore bi P goal p A λ p' A goal' =>
+      iCasesCore hyps goal' arg p' A @k
 
 elab "icases" keep:("+keep")? colGt pmt:pmTerm "with" colGt pat:icasesPat : tactic => do
   -- parse syntax
@@ -243,8 +254,7 @@ elab "icases" keep:("+keep")? colGt pmt:pmTerm "with" colGt pat:icasesPat : tact
   let ⟨_, hyps, p, A, pf⟩ ← iHave hyps pmt (keep.isSome || pmt.is_nontrivial) (try_dup_context := pat.should_try_dup_context)
 
   -- process pattern
-  have ⟨B, eq⟩ := mkIntuitionisticIf bi p A
-  let pf2 ← iCasesCore bi hyps goal p B A eq pat (λ hyps => addBIGoal hyps goal)
+  let pf2 ← iCasesCore bi hyps goal pat p A λ hyps goal => addBIGoal hyps goal
 
   mvar.assign q(($pf).trans $pf2)
 
@@ -252,5 +262,5 @@ macro "imod" colGt pmt:pmTerm "with" colGt pat:icasesPat : tactic => `(tactic |
 macro "imod" colGt hyp:ident : tactic => `(tactic | imod $hyp:ident with $hyp:ident)
 
 -- TODO: remove these shortcuts if they are not used
-macro "iintuitionistic" hyp:ident : tactic => `(tactic | icases $hyp:ident with □$hyp:ident)
+macro "iintuitionistic" hyp:ident : tactic => `(tactic | icases $hyp:ident with #$hyp:ident)
 macro "ispatial" hyp:ident : tactic => `(tactic | icases $hyp:ident with ∗$hyp:ident)
diff --git a/src/Iris/ProofMode/Tactics/Have.lean b/src/Iris/ProofMode/Tactics/Have.lean
index ab32fdac..d0a44e63 100644
--- a/src/Iris/ProofMode/Tactics/Have.lean
+++ b/src/Iris/ProofMode/Tactics/Have.lean
@@ -32,6 +32,5 @@ elab "ihave" colGt pat:icasesPat " : " P:term "$$" spat:specPat : tactic => do
   let P ← elabTermEnsuringTypeQ (← `(iprop($P))) prop
   --  establish `P` with `spat`
   let ⟨_, hyps', p, A, pf⟩ ← iSpecializeCore hyps q(true) q(iprop($P -∗ $P)) [spat] (try_dup_context := pat.should_try_dup_context)
-  have ⟨B, eq⟩ := mkIntuitionisticIf bi p A
-  let pf2 ← iCasesCore bi hyps' goal p B A eq pat (λ hyps => addBIGoal hyps goal)
+  let pf2 ← iCasesCore bi hyps' goal pat p A (addBIGoal · ·)
   mvar.assign q(ihave_assert (($pf).trans $pf2))
diff --git a/src/Iris/ProofMode/Tactics/Intro.lean b/src/Iris/ProofMode/Tactics/Intro.lean
index 96afab0d..f6b1e8ca 100644
--- a/src/Iris/ProofMode/Tactics/Intro.lean
+++ b/src/Iris/ProofMode/Tactics/Intro.lean
@@ -88,7 +88,7 @@ private partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)}
     | .intuitionistic pat, some _ =>
       let .some _ ← ProofModeM.trySynthInstanceQ q(IntoPersistently false $A1 $B)
         | throwError "iintro: {A1} not persistent"
-      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore · A2 pats)
+      let pf ← iCasesCore bi hyps A2 pat q(true) B (iIntroCore · · pats)
       return q(imp_intro_intuitionistic (Q := $Q) $pf)
     | .intuitionistic pat, none =>
       let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q $A1 $A2)
@@ -97,19 +97,19 @@ private partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)}
         | throwError "iintro: {A1} not persistent"
       let .some _ ← trySynthInstanceQ q(TCOr (Affine $A1) (Absorbing $A2))
         | throwError "iintro: {A1} not affine and the goal not absorbing"
-      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore · A2 pats)
+      let pf ← iCasesCore bi hyps A2 pat q(true) B (iIntroCore · · pats)
       return q(wand_intro_intuitionistic (Q := $Q) $pf)
     | _, some _ =>
       -- should always succeed
       let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B $A1)
       let .some _ ← trySynthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P))
         | throwError "iintro: {A1} is not persistent and spatial context is non-empty"
-      let pf ← iCasesCore bi hyps A2 q(false) B B ⟨⟩ pat (iIntroCore · A2 pats)
+      let pf ← iCasesCore bi hyps A2 pat q(false) B (iIntroCore · · pats)
       return q(imp_intro_spatial (Q := $Q) $pf)
     | _, none =>
       let .some _ ← ProofModeM.trySynthInstanceQ q(FromWand $Q $A1 $A2)
         | throwError "iintro: {Q} not a wand"
-      let pf ← iCasesCore bi hyps A2 q(false) A1 A1 ⟨⟩ pat (iIntroCore · A2 pats)
+      let pf ← iCasesCore bi hyps A2 pat q(false) A1 (iIntroCore · · pats)
       return q(wand_intro_spatial (Q := $Q) $pf)
 
 
diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index bed0c9b3..cc3bfd51 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -59,7 +59,7 @@ namespace clear
 
 /-- Tests clearing an intuitionistic hypothesis with `iclear` -/
 example [BI PROP] (P Q : PROP) : □ P ⊢ Q -∗ Q := by
-  iintro □HP
+  iintro #HP
   iintro HQ
   iclear HP
   iexact HQ
@@ -73,7 +73,7 @@ example [BI PROP] (P Q : PROP) : <affine> P ⊢ Q -∗ Q := by
 
 /-- Tests clearing all intuitionistic hypotheses with `iclear #` -/
 example [BI PROP] (P Q R : PROP) : □ P ∗ □ Q ⊢ R -∗ R := by
-  iintro ⟨□HP, □HQ⟩ HR
+  iintro ⟨#HP, #HQ⟩ HR
   iclear #
   iexact HR
 
@@ -97,14 +97,14 @@ example [BI PROP] (φ ψ : Prop) (_hφ : φ) (_hψ : ψ) (Q : PROP) : Q ⊢ Q :=
 
 /-- Tests clearing proofmode and Lean contexts at the same time. -/
 example [BI PROP] (_x : α) (_hφ : φ) (P Q : PROP) : □ P ⊢ Q -∗ Q := by
-  iintro □HP
+  iintro #HP
   iintro HQ
   iclear HP %_x %_hφ
   iexact HQ
 
 /-- Tests clearing `%`, `#`, and `∗` at the same time. -/
 example [BI PROP] (_hφ : φ) (P Q R : PROP) : □ P ∗ <affine> Q ⊢ <affine> R -∗ emp := by
-  iintro ⟨□HP, HQ⟩
+  iintro ⟨#HP, HQ⟩
   iintro HR
   iclear % # ∗
   iemp_intro
@@ -158,14 +158,14 @@ example [BI PROP] (Q : PROP) : Q ⊢ Q := by
   iintro HQ
   iexact HQ
 
-/-- Tests introducing an intuitionistic hypothesis with the `□` pattern -/
+/-- Tests introducing an intuitionistic hypothesis with the `#` pattern -/
 example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
-  iintro □HQ
+  iintro #HQ
   iexact HQ
 
 /-- Tests introducing an affine persistent proposition as intuitionistic -/
 example [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ Q := by
-  iintro □HQ
+  iintro #HQ
   iexact HQ
 
 /-- Tests introducing a persistent implication in the spatial context -/
@@ -175,7 +175,7 @@ example [BI PROP] (Q : PROP) : ⊢ <pers> Q → Q := by
 
 /- Tests introducing an implication in an intuitionistic context -/
 example [BI PROP] (P : PROP) : ⊢ □ P -∗ P → P := by
-  iintro □HP1 HP2
+  iintro #HP1 HP2
   iexact HP2
 
 /-- Tests dropping a hypothesis in an implication with the `-` pattern -/
@@ -196,12 +196,12 @@ example [BI PROP] : ⊢@{PROP} ∀ x, ⌜x = 0⌝ → ⌜x = 0⌝ := by
 
 /-- Tests introducing and extracting a pure hypothesis in affine BI -/
 example [BI PROP] [BIAffine PROP] φ (Q : PROP) : ⊢ ⌜φ⌝ -∗ Q -∗ Q := by
-  iintro ⌜Hφ⌝ HQ
+  iintro %Hφ HQ
   iexact HQ
 
 /-- Tests introducing with disjunction pattern inside intuitionistic -/
 example [BI PROP] (P1 P2 Q : PROP) : □ (P1 ∨ P2) ∗ Q ⊢ Q := by
-  iintro ⟨□(_HP1 | _HP2), HQ⟩
+  iintro ⟨#(_HP1 | _HP2), HQ⟩
   <;> iexact HQ
 
 /-- Tests introducing multiple spatial hypotheses -/
@@ -211,12 +211,12 @@ example [BI PROP] (P Q : PROP) : ⊢ <affine> P -∗ Q -∗ Q := by
 
 /-- Tests introducing multiple intuitionistic hypotheses -/
 example [BI PROP] (Q : PROP) : ⊢ □ P -∗ □ Q -∗ Q := by
-  iintro □_HP □HQ
+  iintro #_HP #HQ
   iexact HQ
 
 /-- Tests introducing with complex nested patterns -/
 example [BI PROP] (Q : PROP) : ⊢ □ (P1 ∧ P2) -∗ Q ∨ Q -∗ Q := by
-  iintro □⟨_HP1, ∗_HP2⟩ (HQ | HQ)
+  iintro #⟨_HP1, ∗_HP2⟩ (HQ | HQ)
   <;> iexact HQ
 
 /- Tests `iintro` failing to introduce pure hypothesis -/
@@ -235,19 +235,19 @@ example [BI PROP] (Q : PROP) : ⊢ Q := by
 /-- error: iintro: Q not a wand -/
 #guard_msgs in
 example [BI PROP] (Q : PROP) : ⊢ Q := by
-  iintro □H
+  iintro #H
 
 /- Tests `iintro` failing to introduce non-intuitionistic wand as intuitionistic -/
 /-- error: iintro: P not persistent -/
 #guard_msgs in
 example [BI PROP] (P Q : PROP) : ⊢ P -∗ Q := by
-  iintro □H
+  iintro #H
 
 /- Tests `iintro` failing to introduce non-intuitionistic implication as intuitionistic -/
 /-- error: iintro: P not persistent -/
 #guard_msgs in
 example [BI PROP] (P Q : PROP) : ⊢ P → Q := by
-  iintro □H
+  iintro #H
 
 /- Tests `iintro` failing to introduce implication with non-empty spatial context -/
 /-- error: iintro: P is not persistent and spatial context is non-empty -/
@@ -277,7 +277,7 @@ example [BI PROP] (P Q : PROP) (H : ⊢ P -∗ Q) : P ⊢ Q := by
 
 /-- Tests `irevert` with a intuitionistic proposition -/
 example [BI PROP] (P : PROP) (H : ⊢ □ P -∗ P) : □ P ⊢ P := by
-  iintro □HP
+  iintro #HP
   irevert HP
   exact H
 
@@ -309,7 +309,7 @@ example [BI PROP] (P Q : PROP) :
 /-- Tests `irevert` with multiple intuitionistic propositions -/
 example [BI PROP] (P Q : PROP) :
     ⊢ (□ P -∗ <affine> Q -∗ P) -∗ □ P -∗ <affine> Q -∗ P := by
-  iintro H □HP HQ
+  iintro H #HP HQ
   irevert HP HQ
   iexact H
 
@@ -321,7 +321,7 @@ example [BI PROP] (P Q : PROP) (H : ⊢ P -∗ <affine> Q -∗ P) : P ∗ <affin
 
 /-- Tests `irevert #` with all intuitionistic hypotheses. -/
 example [BI PROP] (P Q : PROP) (H : ⊢ □ P -∗ □ Q -∗ P) : □ P ∗ □ Q ⊢ P := by
-  iintro ⟨□HP, □HQ⟩
+  iintro ⟨#HP, #HQ⟩
   irevert #
   exact H
 
@@ -333,9 +333,9 @@ example [BI PROP] (P : PROP) (Hφ : φ) (Hψ : ψ) : ⊢ (<affine> ⌜φ⌝ -∗
 
 /-- Tests `irevert % # ∗` with Lean pure, intuitionistic, and spatial hypotheses together. -/
 example {φ ψ : Prop} [BI PROP] (P Q : PROP) (Hφ : φ) (Hψ : ψ) : □ P ∗ <affine> Q ⊢ P := by
-  iintro ⟨□HP, HQ⟩
+  iintro ⟨#HP, HQ⟩
   irevert % # ∗
-  iintro %hφ ⌜hψ⌝ □HP _HQ
+  iintro %hφ %hψ #HP _HQ
   iexact HP
 
 /-- Tests `irevert` with mixed Lean/proofmode hypotheses and dependencies. -/
@@ -458,19 +458,19 @@ example [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ □ Q := by
 
 /-- Tests `iassumption` with intuitionistic hypothesis -/
 example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
-  iintro □_HQ
+  iintro #_HQ
   iassumption
 
 /-- Tests `iassumption` with multiple hypotheses -/
 example [BI PROP] (P Q : PROP) : □ Q ∗ P ⊢ P := by
-  iintro ⟨□_, _⟩
+  iintro ⟨#_, _⟩
   iassumption
 
 /- Tests `iassumption` failure -/
 /-- error: iassumption: no matching assumption -/
 #guard_msgs in
 example [BI PROP] (P Q : PROP) : □ P ⊢ Q := by
-  iintro □_HQ
+  iintro #_HQ
   iassumption
 
 end assumption
@@ -501,7 +501,7 @@ example [BI PROP] (P Q R S : PROP) : ⊢ (P -∗ Q) -∗ P -∗ R -∗ (Q -∗ R
 
 /-- Tests `iapply` with intuitionistic exact -/
 example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
-  iintro □HQ
+  iintro #HQ
   iapply HQ
 
 /-- Tests `iapply` with intuitionistic wand argument -/
@@ -511,7 +511,7 @@ example [BI PROP] (P Q : PROP) : ⊢ □ P -∗ (P -∗ Q) -∗ Q := by
 
 /-- Tests `iapply` with multiple intuitionistic hypotheses and subgoals -/
 example [BI PROP] (P Q R : PROP) : ⊢ □ P -∗ Q -∗ □ (P -∗ Q -∗ □ R) -∗ R := by
-  iintro □HP HQ □H
+  iintro #HP HQ #H
   iapply H $$ [], [HQ] as Q
   case Q => iexact HQ
   iexact HP
@@ -603,7 +603,7 @@ example [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y)
 /-- Tests `iapply` with tactic -/
 example [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
   iintro H HP
-  iapply H $$ %by exact a, %b, [HP]
+  iapply H $$ %(by exact a), %b, [HP]
   iapply HP
 
 /-- Tests `iapply` with pure hypothesis -/
@@ -646,7 +646,7 @@ example [BI PROP] (P Q : α → PROP) (a b : α) : (□ ∀ x, ∀ y, P x -∗ Q
 /-- Tests `iapply` with two wands and subgoals -/
 example [BI PROP] (P Q : Nat → PROP) :
   (P 1 -∗ P 2 -∗ Q 1) ⊢ □ P 1 -∗ P 2 -∗ Q 1 := by
-  iintro H □HP1 HP2
+  iintro H #HP1 HP2
   iapply H
   . iexact HP1
   . iexact HP2
@@ -776,13 +776,13 @@ example [BI PROP] (P Q : α → PROP) (a b : α) : (□ ∀ x, ∀ y, P x -∗ Q
 /-- Tests `ihave` with cases pattern -/
 example [BI PROP] (P Q : PROP) : ⊢ (□P ∗ Q) -∗ Q := by
   iintro H
-  ihave ⟨□_, HQ⟩ := H
+  ihave ⟨#_, HQ⟩ := H
   iexact HQ
 
 /-- Tests `ihave` not removing a destructed hyp -/
 example [BI PROP] [BIAffine PROP] (Q : PROP) :
   □ (Q ∗ Q) ⊢ (□ (Q ∗ Q) ∗ □ Q) ∗ □ Q := by
-  iintro □HQ
+  iintro #HQ
   ihave ⟨HQ, HQ2⟩ := HQ
   istop
   exact .rfl
@@ -799,7 +799,7 @@ example [BI PROP] (P Q : PROP) : ⊢ P -∗ (P -∗ Q) -∗ Q := by
 /-- Tests `ihave` assert duplicating the context -/
 example [BI PROP] (P Q : PROP) (h : P ⊢ □ Q) : ⊢ P -∗ P ∗ Q := by
   iintro HP
-  ihave □HQ : □Q $$ [HP]
+  ihave #HQ : □Q $$ [HP]
   · iapply h $$ HP
   isplitl
   · iexact HP
@@ -918,23 +918,23 @@ namespace spatial
 
 /-- Tests `ispatial` to move hypothesis to spatial context -/
 example [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
-  iintro □HP
-  iintro □HQ
+  iintro #HP
+  iintro #HQ
   ispatial HP
   iexact HQ
 
 /-- Tests `ispatial` with multiple hypotheses -/
 example [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
-  iintro □HP
-  iintro □HQ
+  iintro #HP
+  iintro #HQ
   ispatial HP
   ispatial HQ
   iexact HQ
 
 /-- Tests `ispatial` applied twice to same hypothesis -/
 example [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q := by
-  iintro □HP
-  iintro □HQ
+  iintro #HP
+  iintro #HQ
   ispatial HP
   ispatial HP
   iexact HQ
@@ -970,7 +970,7 @@ example [BI PROP] : ⊢@{PROP} True ∨ False := by
 
 /-- Tests `ipure_intro` with context -/
 example [BI PROP] (H : A → B) (P Q : PROP) : <affine> P ⊢ <pers> Q → ⌜A⌝ → ⌜B⌝ := by
-  iintro _HP □_HQ
+  iintro _HP #_HQ
   ipure_intro
   exact H
 
@@ -1007,38 +1007,38 @@ example [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
 
 /-- Tests `ispecialize` with intuitionistic wand -/
 example [BI PROP] (Q : PROP) : □ P ⊢ □ (P -∗ Q) -∗ □ Q := by
-  iintro □HP □HPQ
+  iintro #HP #HPQ
   ispecialize HPQ $$ HP
   iexact HPQ
 
 /-- Tests `ispecialize` with intuitionistic wand and subgoal -/
 example [BI PROP] (Q : PROP) : □ P ⊢ □ (P -∗ Q) -∗ Q := by
-  iintro □HP □HPQ
+  iintro #HP #HPQ
   ispecialize HPQ $$ []
   . iexact HP
   iexact HPQ
 
 /-- Tests `ispecialize` with intuitionistic wand requiring intuitionistic argument -/
 example [BI PROP] (Q : PROP) : □ P ⊢ □ (□ P -∗ Q) -∗ □ Q := by
-  iintro □HP □HPQ
+  iintro #HP #HPQ
   ispecialize HPQ $$ HP
   iexact HPQ
 
 /-- Tests `ispecialize` with intuitionistic premise and spatial wand -/
 example [BI PROP] (Q : PROP) : □ P ⊢ (P -∗ Q) -∗ Q := by
-  iintro □HP HPQ
+  iintro #HP HPQ
   ispecialize HPQ $$ HP
   iexact HPQ
 
 /-- Tests `ispecialize` with intuitionistic premise required by spatial wand -/
 example [BI PROP] (Q : PROP) : □ P ⊢ (□ P -∗ Q) -∗ Q := by
-  iintro □HP HPQ
+  iintro #HP HPQ
   ispecialize HPQ $$ HP
   iexact HPQ
 
 /-- Tests `ispecialize` with spatial premise and intuitionistic wand -/
 example [BI PROP] (Q : PROP) : P ⊢ □ (P -∗ Q) -∗ Q := by
-  iintro HP □HPQ
+  iintro HP #HPQ
   ispecialize HPQ $$ HP
   iexact HPQ
 
@@ -1059,14 +1059,14 @@ example [BI PROP] (Q : PROP) : ⊢ P1 -∗ P2 -∗ (P1 -∗ P2 -∗ Q) -∗ Q :=
 /-- Tests `ispecialize` with multiple intuitionistic arguments -/
 example [BI PROP] (Q : PROP) :
     ⊢ □ P1 -∗ □ P2 -∗ □ (P1 -∗ □ P2 -∗ Q) -∗ □ Q := by
-  iintro □HP1 □HP2 □HPQ
+  iintro #HP1 #HP2 #HPQ
   ispecialize HPQ $$ HP1, HP2
   iexact HPQ
 
 /-- Tests `ispecialize` with mixed spatial and intuitionistic arguments -/
 example [BI PROP] (Q : PROP) :
     ⊢ P1 -∗ □ P2 -∗ P3 -∗ □ (P1 -∗ P2 -∗ P3 -∗ Q) -∗ Q := by
-  iintro HP1 □HP2 HP3 HPQ
+  iintro HP1 #HP2 HP3 HPQ
   ispecialize HPQ $$ HP1, HP2, HP3
   iexact HPQ
 
@@ -1078,7 +1078,7 @@ example [BI PROP] (Q : Nat → PROP) : ⊢ (∀ x, Q x) -∗ Q (y + 1) := by
 
 /-- Tests `ispecialize` with forall in intuitionistic context -/
 example [BI PROP] (Q : Nat → PROP) : ⊢ □ (∀ x, Q x) -∗ □ Q y := by
-  iintro □HQ
+  iintro #HQ
   ispecialize HQ $$ %y
   iexact HQ
 
@@ -1098,7 +1098,7 @@ example [BI PROP] (Q : Nat → Nat → PROP) :
 /-- Tests `ispecialize` with multiple forall in intuitionistic context -/
 example [BI PROP] (Q : Nat → Nat → PROP) :
     ⊢ □ (∀ x, ∀ y, Q x y) -∗ □ Q x y := by
-  iintro □HQ
+  iintro #HQ
   ispecialize HQ $$ %x, %y
   iexact HQ
 
@@ -1111,7 +1111,7 @@ example [BI PROP] (Q : Nat → Nat → PROP) : ⊢ (∀ x, □ (∀ y, Q x y)) -
 /-- Tests `ispecialize` with mixed forall and wand specialization -/
 example [BI PROP] (Q : Nat → PROP) :
     ⊢ □ P1 -∗ P2 -∗ (□ P1 -∗ (∀ x, P2 -∗ Q x)) -∗ Q y := by
-  iintro □HP1 HP2 HPQ
+  iintro #HP1 HP2 HPQ
   ispecialize HPQ $$ HP1, %y, HP2
   iexact HPQ
 
@@ -1176,7 +1176,7 @@ example [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -∗ P ∗ Q
 /-- Tests `isplitl` without argument -/
 example [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ □ Q -∗ R -∗ P ∗ Q := by
   iintro HP
-  iintro □HQ
+  iintro #HQ
   iintro _HR
   isplitl
   · iexact HP
@@ -1184,7 +1184,7 @@ example [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ □ Q -∗ R -∗ P 
 
 /-- Tests `isplitr` without argument -/
 example [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ □ P -∗ Q -∗ R -∗ P ∗ Q := by
-  iintro □HP
+  iintro #HP
   iintro HQ
   iintro _HR
   isplitr
@@ -1251,7 +1251,7 @@ example [BI PROP] (P Q : PROP) : ⊢ P -∗ <affine> Q -∗ P := by
 
 /-- Tests `icases` with nested conjunction -/
 example [BI PROP] (Q : PROP) : □ (P1 ∧ P2 ∧ Q) ⊢ Q := by
-  iintro □HP
+  iintro #HP
   icases HP with ⟨_HP1, _HP2, HQ⟩
   iexact HQ
 
@@ -1264,7 +1264,7 @@ example [BI PROP] (Q : PROP) : □ P ∧ Q ⊢ Q := by
 /-- Tests `icases` on conjunction with persistent left -/
 example [BI PROP] (Q : PROP) : <pers> Q ∧ <affine> P ⊢ Q := by
   iintro HQP
-  icases HQP with ⟨□HQ, _HP⟩
+  icases HQP with ⟨#HQ, _HP⟩
   iexact HQ
 
 /-- Tests `icases` on conjunction with persistent right -/
@@ -1301,10 +1301,10 @@ example [BI PROP] [BIAffine PROP] (Q : PROP) :
   icases HP with ⟨_HP11 | _HP12 | _HP13, HP2, HP31 | HP32 | HP33, HQ⟩
   <;> iexact HQ
 
-/-- Tests `icases` moving pure to Lean context with ⌜⌝ -/
+/-- Tests `icases` moving pure to Lean context with % -/
 example [BI PROP] (Q : PROP) : ⊢ <affine> ⌜⊢ Q⌝ -∗ Q := by
   iintro HQ
-  icases HQ with ⌜HQ⌝
+  icases HQ with %HQ
   istop
   exact HQ
 
@@ -1315,10 +1315,10 @@ example [BI PROP] (Q : PROP) : ⊢ <affine> ⌜⊢ Q⌝ -∗ Q := by
   istop
   exact HQ
 
-/-- Tests `icases` moving to intuitionistic with □ -/
+/-- Tests `icases` moving to intuitionistic with # -/
 example [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
   iintro HQ
-  icases HQ with □HQ
+  icases HQ with #HQ
   iexact HQ
 
 /-- Tests `icases` moving to intuitionistic with # -/
@@ -1329,20 +1329,20 @@ example [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
 
 /-- Tests `icases` moving to spatial with ∗ -/
 example [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
-  iintro □HQ
+  iintro #HQ
   icases HQ with ∗HQ
   iexact HQ
 
-/-- Tests `icases` moving to spatial with * -/
+/-- Tests `icases` moving to spatial with ∗ only -/
 example [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q := by
-  iintro □HQ
-  icases HQ with *HQ
+  iintro #HQ
+  icases HQ with ∗HQ
   iexact HQ
 
 /-- Tests `icases` with pure in conjunction -/
 example [BI PROP] (Q : PROP) : ⊢ <affine> ⌜φ⌝ ∗ Q -∗ Q := by
   iintro HφQ
-  icases HφQ with ⟨⌜Hφ⌝, HQ⟩
+  icases HφQ with ⟨%Hφ, HQ⟩
   iexact HQ
 
 /-- Tests `icases` with pure in disjunction -/
@@ -1350,43 +1350,43 @@ example [BI PROP] (Q : PROP) :
     ⊢ <affine> ⌜φ1⌝ ∨ <affine> ⌜φ2⌝ -∗ Q -∗ Q := by
   iintro Hφ
   iintro HQ
-  icases Hφ with (⌜Hφ1⌝ | ⌜Hφ2⌝)
+  icases Hφ with (%Hφ1 | %Hφ2)
   <;> iexact HQ
 
 /-- Tests `icases` with intuitionistic in conjunction -/
 example [BI PROP] (Q : PROP) : ⊢ □ P ∗ Q -∗ Q := by
   iintro HPQ
-  icases HPQ with ⟨□_HP, HQ⟩
+  icases HPQ with ⟨#_HP, HQ⟩
   iexact HQ
 
 /-- Tests `icases` with intuitionistic in disjunction -/
 example [BI PROP] (Q : PROP) : ⊢ □ Q ∨ Q -∗ Q := by
   iintro HQQ
-  icases HQQ with (□HQ | HQ)
+  icases HQQ with (#HQ | HQ)
   <;> iexact HQ
 
 /-- Tests `icases` moving to spatial inside intuitionistic conjunction -/
 example [BI PROP] (Q : PROP) : ⊢ □ (P ∧ Q) -∗ Q := by
-  iintro □HPQ
+  iintro #HPQ
   icases HPQ with ⟨_HP, ∗HQ⟩
   iexact HQ
 
 /-- Tests `icases` with or inside intuitionistic, moving one to spatial -/
 example [BI PROP] (Q : PROP) : ⊢ □ (Q ∨ Q) -∗ Q := by
-  iintro □HPQ
+  iintro #HPQ
   icases HPQ with (HQ | ∗HQ)
   <;> iexact HQ
 
 /-- Tests `icases` moving whole hypothesis to intuitionistic then destructing -/
 example [BI PROP] (Q : PROP) : ⊢ □ (P ∧ Q) -∗ Q := by
   iintro HPQ
-  icases HPQ with □⟨_HP, ∗HQ⟩
+  icases HPQ with #⟨_HP, ∗HQ⟩
   iexact HQ
 
 /-- Tests `icases` with or, moving whole to intuitionistic -/
 example [BI PROP] (Q : PROP) : ⊢ □ (Q ∨ Q) -∗ Q := by
   iintro HPQ
-  icases HPQ with □(HQ | ∗HQ)
+  icases HPQ with #(HQ | ∗HQ)
   <;> iexact HQ
 
 /-- Tests `icases` clearing in conjunction -/
@@ -1422,19 +1422,19 @@ example [BI PROP] (Q : PROP) : P1 ∧ P2 ∧ Q ∧ P3 ⊢ Q := by
 
 /-- Tests `icases` destructing intuitionistic conjunction, clearing left -/
 example [BI PROP] (Q : PROP) : □ (P ∧ Q) ⊢ Q := by
-  iintro □HPQ
+  iintro #HPQ
   icases HPQ with ⟨-, HQ⟩
   iexact HQ
 
 /-- Tests `icases` destructing intuitionistic conjunction, clearing right -/
 example [BI PROP] (Q : PROP) : □ (Q ∧ P) ⊢ Q := by
-  iintro □HQP
+  iintro #HQP
   icases HQP with ⟨HQ, -⟩
   iexact HQ
 
 /-- Tests `icases` destructing multiple intuitionistic conjunctions -/
 example [BI PROP] (Q : PROP) : □ (P1 ∧ P2 ∧ Q ∧ P3) ⊢ Q := by
-  iintro □HPQ
+  iintro #HPQ
   icases HPQ with ⟨-, -, HQ, -⟩
   iexact HQ
 
@@ -1447,7 +1447,7 @@ example [BI PROP] (Q : Nat → PROP) : (∃ x, Q x) ⊢ ∃ x, Q x ∨ False :=
 
 /-- Tests `icases` with intuitionistic existential -/
 example [BI PROP] (Q : Nat → PROP) : □ (∃ x, Q x) ⊢ ∃ x, □ Q x ∨ False := by
-  iintro ⟨%x, □H⟩
+  iintro ⟨%x, #H⟩
   iexists x
   ileft
   iexact H
@@ -1459,10 +1459,42 @@ example [BI PROP] P (Q : Nat → PROP) :
   icases Hwand $$ HP with ⟨%_, -, HQ⟩
   iexact HQ
 
+/-- Tests `icases` with a comprehensive nested pattern combining existential, pure,
+intuitionistic, spatial, disjunction, and clearing. -/
+example [BI PROP] (φ : Prop) (Q : PROP) :
+    □ (∃ _ : Nat, ⌜φ⌝ ∧ Q) ∗ (Q ∨ False) ⊢ Q := by
+  iintro H
+  icases H with ⟨#⟨%_, %_hφ, ∗HQ⟩, (HQ' | -)⟩
+  · iexact HQ'
+  · iexact HQ
+
+/-- Tests `icases` with multiple mod patterns -/
+example [BI PROP] [BIUpdate PROP] (P Q : PROP) : (|==> P) ∗ (|==> Q) ⊢ |==> (P ∗ Q) := by
+  iintro H
+  icases H with ⟨>HP, >HQ⟩
+  isplitl [HP]
+  · iexact HP
+  · iexact HQ
+
+/-- Tests `icases` with a comprehensive nested fancy-update pattern combining mask changes,
+existential, pure, disjunction, conjunction, clearing, and multiple mod eliminations. -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+    (E1 E2 E3 : CoPset) (φ : Prop) (P Q : PROP) :
+    (|={E1,E2}=> ∃ _ : Nat, ⌜φ⌝ ∧ P) ∗
+      ((|={E2,E3}=> Q ∗ emp) ∨ (|={E2,E3}=> emp ∗ Q)) ⊢
+      |={E1,E3}=> (P ∗ Q) := by
+  iintro H
+  icases H with ⟨>⟨%_, %_hφ, HP⟩, (>⟨HQ, -⟩ | >⟨-, HQ⟩)⟩
+  all_goals
+    imodintro
+    isplitl [HP]
+    · iexact HP
+    · iexact HQ
+
 /-- Tests `icases` duplicating the context -/
 example [BI PROP] (Q : PROP) (n : Nat) :
   □ (∀ x, Q -∗ ⌜x = n⌝) ⊢ Q -∗ False := by
-  iintro □Hwand HQ
+  iintro #Hwand HQ
   icases Hwand $$ %1, HQ with %_
   icases Hwand $$ %2, HQ with %_
   grind
@@ -1470,7 +1502,7 @@ example [BI PROP] (Q : PROP) (n : Nat) :
 /-- Tests `icases` removing a destructed hyp -/
 example [BI PROP] [BIAffine PROP] (Q : PROP) :
   □ (Q ∗ Q) ⊢ □ Q ∗ □ Q := by
-  iintro □HQ
+  iintro #HQ
   icases HQ with ⟨HQ, HQ2⟩
   istop
   exact .rfl
@@ -1507,24 +1539,24 @@ section imodintro
 
 /-- Tests `imodintro` for absorbing (intuitionistic: id, spatial: id) -/
 example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro
   iexact HP2
 
 /-- Tests `iintro` for introducing modalities -/
 example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
-  iintro ⟨□HP1, HP2⟩ !>
+  iintro ⟨#HP1, HP2⟩ !>
   iexact HP2
 
 /-- Tests `imodintro` for persistently (intuitionistic: id, spatial: clear) -/
 example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <pers> P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro
   iexact HP1
 
 /-- Tests `imodintro` for affinely (intuitionistic: id, spatial: forall Affine) -/
 example [BI PROP] (P : PROP) : □ P ∗ <affine> P ⊢ <affine> P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro
   iexact HP2
 
@@ -1532,12 +1564,12 @@ example [BI PROP] (P : PROP) : □ P ∗ <affine> P ⊢ <affine> P := by
 /-- error: imodintro: hypothesis HP2 : P does not satisfy Affine -/
 #guard_msgs in
 example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <affine> P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro
 
 /-- Tests `imodintro` for intuitionistically (intuitionistic: id, spatial: isEmpty) -/
 example [BI PROP] (P : PROP) : □ P ∗ □ P ⊢ □ P := by
-  iintro ⟨□HP1, □HP2⟩
+  iintro ⟨#HP1, #HP2⟩
   imodintro
   iexact HP2
 
@@ -1545,36 +1577,36 @@ example [BI PROP] (P : PROP) : □ P ∗ □ P ⊢ □ P := by
 /-- error: imodintro: spatial context is not empty -/
 #guard_msgs in
 example [BI PROP] (P : PROP) : □ P ∗ □ P ⊢ □ P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro
 
 /-- Tests `imodintro` for plain (intuitionistic: .forall Plain, spatial: clear) -/
 example [Sbi PROP] (P : PROP) [Plain P] : □ P ∗ P ⊢ ■ P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro
   iexact HP1
 
 /-- Tests `imodintro` for bupd (intuitionistic: id, spatial: id) -/
 example [BI PROP] [BIUpdate PROP] (P : PROP) : □ P ∗ P ⊢ |==> P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro
   iexact HP2
 
 /-- Tests `imodintro` for later (both: transform) -/
 example [BI PROP] (P : PROP) : □ ▷ P ∗ ▷ P ⊢ ▷ P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro
   iexact HP2
 
 /-- Tests `imodintro` for later n (both: transform) -/
 example [BI PROP] (P : PROP) : □ ▷^[n] P ∗ ▷^[n] P ⊢ ▷^[n] P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro
   iexact HP2
 
 /-- Tests `imodintro` for later n (NatCancel) -/
 example [BI PROP] (P : PROP) : □ ▷^[5] P ∗ ▷^[3] P ⊢ ▷^[4] P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro
   iexact HP2
 
@@ -1587,7 +1619,7 @@ example [BI PROP] (P : PROP) : □ ▷^[n] P ∗ ▷^[n] P ⊢ ▷^[n] P := by
 
 /-- Tests `imodintro` with specifying the pattern -/
 example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro (<absorb> _)
   iexact HP2
 
@@ -1595,7 +1627,7 @@ example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
 /-- error: imodintro: P is not a modality -/
 #guard_msgs in
 example [BI PROP] (P : PROP) : □ P ∗ P ⊢ P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro
 
 /- Tests `imodintro` with specifying the wrong pattern -/
@@ -1603,12 +1635,99 @@ set_option pp.mvars false in
 /-- error: imodintro: iprop(<absorb> P) is not a modality matching iprop(□ ?_) -/
 #guard_msgs in
 example [BI PROP] (P : PROP) : □ P ∗ P ⊢ <absorb> P := by
-  iintro ⟨□HP1, HP2⟩
+  iintro ⟨#HP1, HP2⟩
   imodintro (□ _)
 
 /-- Tests `imodintro` with nested modalities -/
 example [BI PROP] (P : PROP) : □ P ⊢ □ <pers> P := by
-  iintro □HP
+  iintro #HP
+  imodintro
+  imodintro
+  iexact HP
+
+/-- Tests `imodintro` for bupd with single hypothesis -/
+example [BI PROP] [BIUpdate PROP] (P : PROP) : P ⊢ |==> P := by
+  iintro HP
+  imodintro
+  iexact HP
+
+/-- Tests `imodintro` for fupd -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+    (E : CoPset) (P : PROP) : P ⊢ |={E}=> P := by
+  iintro HP
+  imodintro
+  iexact HP
+
+/-- Tests `imodintro` for bupd preserves both intuitionistic and spatial -/
+example [BI PROP] [BIUpdate PROP] (P Q : PROP) : □ P ∗ Q ⊢ |==> Q := by
+  iintro ⟨#HP, HQ⟩
+  imodintro
+  iexact HQ
+
+/-- Tests `imodintro` for persistently with only intuitionistic context -/
+example [BI PROP] (P : PROP) : □ P ∗ □ P ⊢ <pers> P := by
+  iintro ⟨#HP1, #HP2⟩
+  imodintro
+  iexact HP1
+
+/-- Tests `imodintro` for nested bupd -/
+example [BI PROP] [BIUpdate PROP] (P : PROP) : P ⊢ |==> |==> P := by
+  iintro HP
+  imodintro
+  imodintro
+  iexact HP
+
+/-- Tests `imodintro` for later with multiple later hypotheses -/
+example [BI PROP] (P Q : PROP) : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) := by
+  iintro ⟨HP, HQ⟩
+  imodintro
+  isplitl [HP]
+  · iexact HP
+  · iexact HQ
+
+/-- Tests `imodintro` for later with intuitionistic later hypothesis -/
+example [BI PROP] (P : PROP) : □ ▷ P ∗ ▷ P ⊢ ▷ P := by
+  iintro ⟨#HP, HQ⟩
+  imodintro
+  iexact HQ
+
+/-- Tests `imodintro` followed by `imod` -/
+example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> P ⊢ |==> P := by
+  iintro HP
+  imod HP
+  imodintro
+  iexact HP
+
+/-- Tests `imodintro` with explicit pattern for persistently -/
+example [BI PROP] (P : PROP) : □ P ⊢ <pers> P := by
+  iintro #HP
+  imodintro (<pers> _)
+  iexact HP
+
+/-- Tests `imodintro` for affinely with multiple spatial hypotheses -/
+example [BI PROP] (P Q : PROP) [Affine P] [Affine Q] : <affine> P ∗ <affine> Q ⊢ <affine> P := by
+  iintro ⟨HP, HQ⟩
+  imodintro
+  iexact HP
+
+/-- Tests `imodintro` for triple nested modalities -/
+example [BI PROP] (P : PROP) : □ P ⊢ □ <pers> <absorb> P := by
+  iintro #HP
+  imodintro
+  imodintro
+  imodintro
+  iexact HP
+
+/-- Tests `inext` as shorthand for imodintro on later goals -/
+example [BI PROP] (P : PROP) : ▷ P ⊢ ▷ P := by
+  iintro HP
+  inext
+  iexact HP
+
+/-- Tests `imodintro` for fupd then bupd -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+    (E : CoPset) (P : PROP) : P ⊢ |={E}=> |==> P := by
+  iintro HP
   imodintro
   imodintro
   iexact HP
@@ -1623,6 +1742,13 @@ example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> P ⊢ |==> P := by
   imod HP
   iexact HP
 
+/-- Tests `imod` for fupd -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+    (E : CoPset) (P : PROP) : ((|={E}=> P) ⊢ (|={E}=> P)) := by
+  iintro HP
+  imod HP
+  iexact HP
+
 /-- Tests `imod` removing later before timeless propositions -/
 example [BI PROP] [BIUpdate PROP] (P : PROP) [Timeless P] : ▷ P ⊢ ◇ P := by
   iintro HP
@@ -1636,18 +1762,40 @@ example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> P ⊢ emp -∗ |==> P := by
   iintro _
   iexact HP
 
+/-- Tests `imod` for fupd under wand -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+    (E : CoPset) (P : PROP) : (|={E}=> P) ⊢ emp -∗ |={E}=> P := by
+  iintro HP
+  imod HP
+  iintro _
+  iexact HP
+
 /-- Tests `imod` with destructuring pattern -/
 example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> (P ∗ emp) ⊢ |==> P := by
   iintro HP
   imod HP with ⟨HP, _⟩
   iexact HP
 
+/-- Tests `imod` with destructuring pattern for fupd -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+    (E : CoPset) (P : PROP) : (|={E}=> P ∗ emp) ⊢ |={E}=> P := by
+  iintro HP
+  imod HP with ⟨HP, _⟩
+  iexact HP
+
 /-- Tests `icases` with mod pattern -/
 example [BI PROP] [BIUpdate PROP] (P : PROP) : emp ∗ |==> P ⊢ |==> P := by
   iintro HP
   icases HP with ⟨_, >HP⟩
   iexact HP
 
+/-- Tests `icases` with mod pattern for fupd -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+    (E : CoPset) (P : PROP) : emp ∗ (|={E}=> P) ⊢ |={E}=> P := by
+  iintro HP
+  icases HP with ⟨_, >HP⟩
+  iexact HP
+
 /- Tests `imod` for no modality -/
 /-- error: imod: P is not a modality -/
 #guard_msgs in
@@ -1662,6 +1810,48 @@ example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> |==> P ⊢ |==> P := by
   imod HP
   iexact HP
 
+/-- Tests `imod` eliminating nested fupd modalities -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+    (E : CoPset) (P : PROP) : (|={E}=> |={E}=> P) ⊢ |={E}=> P := by
+  iintro HP
+  imod HP
+  imod HP
+  iexact HP
+
+/-- Tests `imod` for nested mask-changing fupd. -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP]
+    (E1 E2 E3 : CoPset) (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P := by
+  iintro HP
+  imod HP
+  iexact HP
+
+/-- Tests `imod` with destructuring nested separating conjunction -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+    (E1 E2 : CoPset) (P Q R : PROP) :
+    (|={E1,E2}=> P ∗ Q ∗ R) ⊢ |={E1,E2}=> (P ∗ Q ∗ R) := by
+  iintro HP
+  imod HP with ⟨HP, HQ, HR⟩
+  isplitl [HP]
+  · iexact HP
+  isplitl [HQ]
+  · iexact HQ
+  · iexact HR
+
+/-- Tests `imod` for later with timeless under except0 goal -/
+example [BI PROP] (P Q : PROP) [Timeless P] : ▷ P ∗ Q ⊢ ◇ (P ∗ Q) := by
+  iintro ⟨HP, HQ⟩
+  imod HP
+  isplitl [HP]
+  · iexact HP
+  · iexact HQ
+
+/-- Tests `imod` for fupd with intuitionistic hypothesis -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+    (E : CoPset) (P : PROP) : □ (|={E}=> P) ⊢ |={E}=> P := by
+  iintro #HP
+  imod HP
+  iexact HP
+
 end imod
 
 section inext
diff --git a/tactics.md b/tactics.md
index f451d8cc..f7eceb4a 100644
--- a/tactics.md
+++ b/tactics.md
@@ -11,7 +11,7 @@
 | `iassumption`                              | Solve the goal with a hypothesis from any context (pure, intuitionistic or spatial).                                                                                                                                                 |
 | `iex_falso`                                | Change the goal to `False`.                                                                                                                                                                                                          |
 | `ipure` *hyp*                              | Move the hypothesis *hyp* to the pure context.                                                                                                                                                                                       |
-| `iintuitionistic` *hyp*                    | Move the hypothesis *hyp* to the intuitionistic context.                                                                                                                                                                             |
+| `iintuitionistic` *hyp*                    | Move the hypothesis *hyp* to the intuitionistic context. Equivalent to `icases hyp with #hyp`.                                       |
 | `ispatial` *hyp*                           | Move the hypothesis *hyp* to the spatial context.                                                                                                                                                                                    |
 | `iemp_intro`                               | Solve the goal if it is `emp` and discard all hypotheses.                                                                                                                                                                            |
 | `ipure_intro`                              | Turn a goal of the form `⌜φ⌝` into a Lean goal `φ`.                                                                                                                                                                                  |
@@ -35,20 +35,22 @@
 | Pattern                         | Description                                                                                                                                                                         |
 |---------------------------------|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
 | *name*                          | Rename the hypothesis to *name*.                                                                                                                                                    |
-| `_`                             | Drop the hypothesis.                                                                                                                                                                |
+| `-`                             | Drop the hypothesis.                                                                                                                                                                |
 | `⟨`*pat_1* [`,` *pat_2*]...`⟩`  | Destruct a (separating) conjunction and recursively destruct its arguments using the patterns *pat_i*.                                                                              |
 | `(`*pat_1* [`\|` *pat_2*]...`)` | Destruct a disjunction and recursively destruct its arguments in separate goals using the patterns *pat_i*. The parentheses can be omitted if this pattern is not on the top level. |
-| `⌜`*name*`⌝`                    | Move the hypothesis to the pure context and rename it to *name*.                                                                                                                    |
-| `□` *pat*                       | Move the hypothesis to the intuitionistic context and further destruct it using the pattern *pat*.                                                                                  |
-| `∗` *pat*                      | Move the hypothesis to the spatial context and further destruct it using the pattern *pat*.                                                                                         |
-| `>` *pat*                       | Eliminate the modality at the top of the hypothesis and further destruct the result using the pattern *pat*.                                                                        |
+| `%`*name*                       | Move the hypothesis to the pure context and rename it to *name*.                                                                                                                    |
+| `#`*pat*                        | Move the hypothesis to the intuitionistic context and further destruct it using the pattern *pat*.                                                                                  |
+| `∗`*pat*                        | Move the hypothesis to the spatial context and further destruct it using the pattern *pat*.                                                                                         |
+| `>`*pat*                        | Eliminate the modality at the top of the hypothesis and further destruct the result using the pattern *pat*.                                                                        |
+
+The supported shorthand patterns are `%` for pure hypotheses and `#` for intuitionistic ones. The older spellings `⌜name⌝`, `□pat`, and `*pat` are no longer supported.
 
 Example:
 ```lean
 -- the hypothesis:
 P1 ∗ (□ P2 ∨ P2) ∗ (P3 ∧ P3')
 -- can be destructed using the pattern:
-⟨HP1, □HP2 | HP2, ⟨HP3, _⟩⟩
+⟨HP1, #HP2 | HP2, ⟨HP3, -⟩⟩
 -- (there are of course other valid patterns for destructing the shown hypothesis)
 ```
 

From cb26b842ca98f162dd010fcf7cee45497237b909 Mon Sep 17 00:00:00 2001
From: HaleOIC <yunsongyang730@gmail.com>
Date: Wed, 8 Apr 2026 16:05:50 +0200
Subject: [PATCH 2/7] typo

---
 src/Iris/Tests/Tactics.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index a3049b21..9e85be1b 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -512,7 +512,7 @@ example [BI PROP] (P Q : PROP) : ⊢ □ P -∗ (P -∗ Q) -∗ Q := by
 /-- Tests `iapply` with multiple intuitionistic hypotheses and subgoals -/
 example [BI PROP] (P Q R : PROP) : ⊢ □ P -∗ Q -∗ □ (P -∗ Q -∗ □ R) -∗ R := by
   iintro #HP HQ #H
-  iapply H $$ [], [HQ] as Q
+  iapply H $$ [] [HQ] as Q
   case Q => iexact HQ
   iexact HP
 

From 2518658e6d74d7d2c378f2ccde50f1a30da76835 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 8 Apr 2026 16:47:25 +0200
Subject: [PATCH 3/7] small tweak to tests

---
 src/Iris/Tests/Tactics.lean | 36 ++++++++++++++++++++++++------------
 1 file changed, 24 insertions(+), 12 deletions(-)

diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index 9e85be1b..5868136d 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -427,6 +427,12 @@ example [BI PROP] (Q : PROP) : □ Q ⊢ Q := by
   iintro HQ
   iexact HQ
 
+/-- Tests `iexact` with fupd -/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+    (E : CoPset) (P : PROP) : P ⊢ |={E}=> P := by
+  iintro HP
+  iexact HP
+
 /- Tests `iexact` failing with not-affine assumption -/
 /-- error: iexact: context is not affine or goal is not absorbing -/
 #guard_msgs in
@@ -1652,7 +1658,7 @@ example [BI PROP] [BIUpdate PROP] (P : PROP) : P ⊢ |==> P := by
   iexact HP
 
 /-- Tests `imodintro` for fupd -/
-example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+example [BI PROP] [BIFUpdate PROP]
     (E : CoPset) (P : PROP) : P ⊢ |={E}=> P := by
   iintro HP
   imodintro
@@ -1725,7 +1731,7 @@ example [BI PROP] (P : PROP) : ▷ P ⊢ ▷ P := by
   iexact HP
 
 /-- Tests `imodintro` for fupd then bupd -/
-example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP]
     (E : CoPset) (P : PROP) : P ⊢ |={E}=> |==> P := by
   iintro HP
   imodintro
@@ -1743,10 +1749,11 @@ example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> P ⊢ |==> P := by
   iexact HP
 
 /-- Tests `imod` for fupd -/
-example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
-    (E : CoPset) (P : PROP) : ((|={E}=> P) ⊢ (|={E}=> P)) := by
+example [BI PROP] [BIFUpdate PROP]
+    (E : CoPset) (P : PROP) : (|={E}=> P) ⊢ |={E}=> P := by
   iintro HP
   imod HP
+  imodintro
   iexact HP
 
 /-- Tests `imod` removing later before timeless propositions -/
@@ -1763,11 +1770,11 @@ example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> P ⊢ emp -∗ |==> P := by
   iexact HP
 
 /-- Tests `imod` for fupd under wand -/
-example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+example [BI PROP] [BIFUpdate PROP]
     (E : CoPset) (P : PROP) : (|={E}=> P) ⊢ emp -∗ |={E}=> P := by
   iintro HP
   imod HP
-  iintro _
+  iintro _ !>
   iexact HP
 
 /-- Tests `imod` with destructuring pattern -/
@@ -1777,10 +1784,11 @@ example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> (P ∗ emp) ⊢ |==> P := by
   iexact HP
 
 /-- Tests `imod` with destructuring pattern for fupd -/
-example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+example [BI PROP] [BIFUpdate PROP]
     (E : CoPset) (P : PROP) : (|={E}=> P ∗ emp) ⊢ |={E}=> P := by
   iintro HP
   imod HP with ⟨HP, _⟩
+  imodintro
   iexact HP
 
 /-- Tests `icases` with mod pattern -/
@@ -1790,10 +1798,11 @@ example [BI PROP] [BIUpdate PROP] (P : PROP) : emp ∗ |==> P ⊢ |==> P := by
   iexact HP
 
 /-- Tests `icases` with mod pattern for fupd -/
-example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+example [BI PROP] [BIFUpdate PROP]
     (E : CoPset) (P : PROP) : emp ∗ (|={E}=> P) ⊢ |={E}=> P := by
   iintro HP
   icases HP with ⟨_, >HP⟩
+  imodintro
   iexact HP
 
 /- Tests `imod` for no modality -/
@@ -1811,26 +1820,28 @@ example [BI PROP] [BIUpdate PROP] (P : PROP) : |==> |==> P ⊢ |==> P := by
   iexact HP
 
 /-- Tests `imod` eliminating nested fupd modalities -/
-example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+example [BI PROP] [BIFUpdate PROP]
     (E : CoPset) (P : PROP) : (|={E}=> |={E}=> P) ⊢ |={E}=> P := by
   iintro HP
   imod HP
   imod HP
+  imodintro
   iexact HP
 
 /-- Tests `imod` for nested mask-changing fupd. -/
-example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP]
+example [BI PROP] [BIFUpdate PROP]
     (E1 E2 E3 : CoPset) (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P := by
   iintro HP
   imod HP
   iexact HP
 
 /-- Tests `imod` with destructuring nested separating conjunction -/
-example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+example [BI PROP] [BIFUpdate PROP]
     (E1 E2 : CoPset) (P Q R : PROP) :
     (|={E1,E2}=> P ∗ Q ∗ R) ⊢ |={E1,E2}=> (P ∗ Q ∗ R) := by
   iintro HP
   imod HP with ⟨HP, HQ, HR⟩
+  imodintro
   isplitl [HP]
   · iexact HP
   isplitl [HQ]
@@ -1846,10 +1857,11 @@ example [BI PROP] (P Q : PROP) [Timeless P] : ▷ P ∗ Q ⊢ ◇ (P ∗ Q) := b
   · iexact HQ
 
 /-- Tests `imod` for fupd with intuitionistic hypothesis -/
-example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] [BIUpdateFUpdate PROP]
+example [BI PROP] [BIFUpdate PROP]
     (E : CoPset) (P : PROP) : □ (|={E}=> P) ⊢ |={E}=> P := by
   iintro #HP
   imod HP
+  imodintro
   iexact HP
 
 end imod

From 353aabdaa1e41b67aef7640b1c2f3dfa75ec97cb Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 8 Apr 2026 16:50:24 +0200
Subject: [PATCH 4/7] tweak tactics.md

---
 tactics.md | 2 --
 1 file changed, 2 deletions(-)

diff --git a/tactics.md b/tactics.md
index 2c8d6d20..e03e2c0c 100644
--- a/tactics.md
+++ b/tactics.md
@@ -43,8 +43,6 @@
 | `∗`*pat*                        | Move the hypothesis to the spatial context and further destruct it using the pattern *pat*.                                                                                         |
 | `>`*pat*                        | Eliminate the modality at the top of the hypothesis and further destruct the result using the pattern *pat*.                                                                        |
 
-The supported shorthand patterns are `%` for pure hypotheses and `#` for intuitionistic ones. The older spellings `⌜name⌝`, `□pat`, and `*pat` are no longer supported.
-
 Example:
 ```lean
 -- the hypothesis:

From aa4994e203152547f25c80a556876ece435c0aa8 Mon Sep 17 00:00:00 2001
From: HaleOIC <yunsongyang730@gmail.com>
Date: Thu, 9 Apr 2026 11:04:33 +0200
Subject: [PATCH 5/7] complete mask manipulation theorem in updates

---
 src/Iris/BI/Updates.lean                 | 61 +++++++++++++++++-------
 src/Iris/ProofMode/InstancesUpdates.lean | 16 ++-----
 src/Iris/Std/Classes.lean                |  6 +++
 src/Iris/Std/CoPset.lean                 |  3 ++
 src/Iris/Std/GenSets.lean                | 11 +++++
 5 files changed, 68 insertions(+), 29 deletions(-)

diff --git a/src/Iris/BI/Updates.lean b/src/Iris/BI/Updates.lean
index d8f9a0ea..e91a08ab 100644
--- a/src/Iris/BI/Updates.lean
+++ b/src/Iris/BI/Updates.lean
@@ -192,7 +192,7 @@ section FUpdLaws
 
 variable [BI PROP] [BIFUpdate PROP]
 
-open BIFUpdate
+open BIFUpdate LawfulSet
 
 theorem fupd_mask_intro_subseteq {E1 E2 : CoPset} {P : PROP} : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P :=
   λ h => (emp_sep.2.trans <| sep_mono_l <| subset h).trans <|
@@ -254,22 +254,47 @@ theorem fupd_mask_frame_r {E1 E2 Ef : CoPset} {P : PROP} :
     E1 ## Ef → (|={E1,E2}=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P :=
   λ h => (mono <| imp_intro' and_elim_r).trans <| mask_frame_r' h
 
--- TODO: the following theorems can be proved only with CoPSet extensional-equality
--- theorem fupd_mask_frame {E E' E1 E2 : CoPset} {P : PROP} :
---     E1 ⊆ E → (|={E1,E2}=> |={E2 ∪ (E \ E1),E'}=> P) ⊢ |={E,E'}=> P := sorry
-
--- theorem fupd_mask_frame_acc {E E' E1 E2 : CoPset} {P Q : PROP}:
---     E1 ⊆ E →
---     (|={E1,E1 \ E2}=> Q) ⊢
---     (Q -∗ |={E \ E2,E'}=> (∀ R, (|={E1 \ E2,E1}=> R) -∗ |={E \ E2,E}=> R) -∗  P) -∗
---     (|={E,E'}=> P) := sorry
-
--- theorem fupd_mask_mono {E1 E2 : CoPset} {P : PROP} :
---     E1 ⊆ E2 → (|={E1}=> P) ⊢ |={E2}=> P := sorry
-
--- theorem fupd_mask_subseteq_emptyset_difference {E1 E2 : CoPset} :
---     E2 ⊆ E1 → ⊢ |={E1,E2}=> |={∅,E1\E2}=> (emp: PROP) := sorry
-
--- theorem fupd_trans_frame {E1 E2 E3 : CoPset} {P Q : PROP} : ((Q ={E2,E3}=∗ emp) ∗ |={E1,E2}=> (Q ∗ P)) ⊢ |={E1,E3}=> P := sorry
+theorem fupd_mask_mono {E1 E2 : CoPset} {P : PROP} :
+    E1 ⊆ E2 → (|={E1}=> P) ⊢ |={E2}=> P :=
+  λ h => by simpa [subset_union_diff h] using
+    (fupd_mask_frame_r (E2 := E1) (Ef := E2 \ E1) disjoint_diff_right)
+
+theorem fupd_mask_frame {E E' E1 E2 : CoPset} {P : PROP} :
+    E1 ⊆ E → (|={E1,E2}=> |={E2 ∪ (E \ E1),E'}=> P) ⊢ |={E,E'}=> P :=
+  λ h => by simpa [subset_union_diff h] using
+    ((fupd_mask_frame_r (P := iprop(|={E2 ∪ (E \ E1),E'}=> P)) disjoint_diff_right).trans trans)
+
+/-- A variant of [fupd_mask_frame] that works well for accessors:
+  Tailored to eliminate updates of the form [|={E1,E1∖E2}=> Q] and provides a way to transform the
+  closing view shift instead of letting you prove the same side-conditions twice. -/
+theorem fupd_mask_frame_acc {E E' E1 E2 : CoPset} {P Q : PROP}:
+    E1 ⊆ E → (|={E1,E1 \ E2}=> Q) ⊢
+    (Q -∗ |={E \ E2,E'}=> (∀ R, (|={E1 \ E2,E1}=> R) -∗ |={E \ E2,E}=> R) -∗  P) -∗
+    (|={E,E'}=> P) := λ hE => by
+  have hmask : E \ E2 ⊆ (E1 \ E2) ∪ (E \ E1) := by
+    intro x hx; rw [mem_diff] at hx
+    by_cases hx1 : x ∈ E1
+    · exact mem_union.2 <| .inl <| mem_diff.2 ⟨hx1, hx.2⟩
+    · exact mem_union.2 <| .inr <| mem_diff.2 ⟨hx.1, hx1⟩
+  have hdisj : (E1 \ E2) ## (E \ E1) := disjoint_subset_left diff_subset_left disjoint_diff_right
+  refine wand_intro <| fupd_frame_r.trans <| (BIFUpdate.mono wand_elim_r).trans ?_
+  refine (BIFUpdate.mono ?_).trans <| fupd_mask_frame hE
+  refine sep_emp.2.trans <| (sep_mono_r <| fupd_mask_intro_subseteq hmask).trans ?_
+  refine fupd_frame_l.trans <| (BIFUpdate.mono fupd_frame_r).trans <| fupd_elim ?_
+  refine BIFUpdate.mono <| sep_symm.trans ?_
+  refine (sep_mono ?_ .rfl).trans wand_elim_r
+  refine forall_intro λ R => wand_intro <| fupd_frame_r.trans <| fupd_elim ?_
+  exact emp_sep.1.trans <| (fupd_mask_frame_r hdisj).trans <| by simp [subset_union_diff hE]
+
+theorem fupd_mask_subseteq_emptyset_difference {E1 E2 : CoPset} :
+    E2 ⊆ E1 → ⊢ |={E1,E2}=> |={∅,E1\E2}=> (emp: PROP) :=
+  λ h => by
+    simpa [union_comm, subset_union_diff h] using (fupd_mask_intro_subseteq empty_subset).trans <|
+      fupd_mask_frame_r (P := iprop(|={∅,E1 \ E2}=> (emp : PROP))) (disjoint_symm <| disjoint_diff_right)
+
+theorem fupd_trans_frame {E1 E2 E3 : CoPset} {P Q : PROP} :
+    ((Q ={E2,E3}=∗ emp) ∗ |={E1,E2}=> (Q ∗ P)) ⊢ |={E1,E3}=> P :=
+  fupd_frame_l.trans <| fupd_elim <| ((sep_assoc.2.trans <| sep_mono_l sep_comm.1).trans <|
+    sep_mono_l wand_elim_r).trans <| fupd_frame_r.trans <| BIFUpdate.mono emp_sep.1
 
 end FUpdLaws
diff --git a/src/Iris/ProofMode/InstancesUpdates.lean b/src/Iris/ProofMode/InstancesUpdates.lean
index 588db221..871a6d5e 100644
--- a/src/Iris/ProofMode/InstancesUpdates.lean
+++ b/src/Iris/ProofMode/InstancesUpdates.lean
@@ -163,7 +163,11 @@ section SBIFancyUpdate
 
 variable {PROP} [Sbi PROP] [BIFUpdate PROP] [BIFUpdatePlainly PROP] [BIAffine PROP]
 
--- instance fromForall_fupd E1 E2 (P : PROP) (Φ : α → PROP)
+-- TODO:
+-- `fromForall_fupd` needs a derived plain/fupd/forall lemma.
+-- `fromForall_stepFupd` additionally needs a step-fupd/forall theorem in `BI/Updates.lean`.
+-- instance fromForall_fupd E1 E2 (P : PROP) {α : Type _} (Φ : α → PROP)
+--     [hmask : TCOr (E1 = E2) (TCOr (E1 = ⊤) (E2 = ∅))]
 --     [h : FromForall P Φ] [∀ a, Plain (Φ a)] :
 --     FromForall iprop(|={E1,E2}=> P) (fun a => iprop(|={E1,E2}=> Φ a)) where
 --   from_forall := sorry
@@ -173,14 +177,4 @@ variable {PROP} [Sbi PROP] [BIFUpdate PROP] [BIFUpdatePlainly PROP] [BIAffine PR
 --     FromForall iprop(|={E}▷=> P) (fun a => iprop(|={E}▷=> Φ a)) where
 --   from_forall := sorry
 
--- @[ipm_backtrack]
--- instance elimModal_fupd_plain_goal p E (P Q : PROP) [Plain Q] :
---     ElimModal True p false iprop(|={E}=> P) P Q Q where
---   elim_modal _ := sorry
-
--- @[ipm_backtrack]
--- instance elimModal_fupd_plain p E (P Q : PROP) [Plain P] :
---     ElimModal True p p iprop(|={E}=> P) P Q Q where
---   elim_modal _ := sorry
-
 end SBIFancyUpdate
diff --git a/src/Iris/Std/Classes.lean b/src/Iris/Std/Classes.lean
index c9e76b75..f4217a3e 100644
--- a/src/Iris/Std/Classes.lean
+++ b/src/Iris/Std/Classes.lean
@@ -12,6 +12,12 @@ namespace Iris.Std
 /-- Represents a binary relation with two arguments of the same type `α`. -/
 abbrev Relation (α : Type _) := α → α → Prop
 
+/-- Require that a type `α` has a distinguished top element. -/
+class Top (α : Type u) where
+  top : α
+export Top (top)
+
+notation "⊤" => top
 
 /-- Require that a relation `R` on `a` is reflexive. -/
 class Reflexive (R : Relation α) where
diff --git a/src/Iris/Std/CoPset.lean b/src/Iris/Std/CoPset.lean
index d6267ae6..b0cef05b 100644
--- a/src/Iris/Std/CoPset.lean
+++ b/src/Iris/Std/CoPset.lean
@@ -6,6 +6,7 @@ Authors: Remy Seassau, Markus de Medeiros, Sergei Stepanenko
 module
 
 public import Iris.Std.Positives
+public import Iris.Std.Classes
 public import Iris.Std.GenSets
 
 @[expose] public section
@@ -218,6 +219,8 @@ instance : EmptyCollection CoPset where emptyCollection := CoPset.empty
 
 def full : CoPset := ⟨CoPsetRaw.leaf true, rfl⟩
 
+instance : Iris.Std.Top CoPset where top := CoPset.full
+
 @[simp] def singleton (p : Pos) : CoPset := ⟨CoPsetRaw.Singleton p, coPsetSingleton_wf p⟩
 
 instance : Singleton Pos CoPset where
diff --git a/src/Iris/Std/GenSets.lean b/src/Iris/Std/GenSets.lean
index 140b0c6b..4e47879f 100644
--- a/src/Iris/Std/GenSets.lean
+++ b/src/Iris/Std/GenSets.lean
@@ -441,6 +441,12 @@ theorem diff_subset_left {s₁ s₂ : S} : s₁ \ s₂ ⊆ s₁ := by
   intro y G; rw [mem_diff] at G
   exact G.left
 
+/-- A set is disjoint from the part removed by taking a difference. -/
+theorem disjoint_diff_right {s₁ s₂ : S} : s₁ ## (s₂ \ s₁) := by
+  intro x ⟨hx1, hx2⟩
+  rw [mem_diff] at hx2
+  exact hx2.2 hx1
+
 /-- Difference with disjoint set is identity. -/
 theorem diff_subset_disj {s₁ s₂ : S} (H : s₁ ## s₂) : s₁ \ s₂ = s₁ := by
   ext x; rw [mem_diff]
@@ -462,6 +468,11 @@ theorem diff_subset_decomp {s₁ s₂ : S} (H : s₁ ⊆ s₂) : s₂ = (s₂ \
   · exact .inr J
   · exact .inl ⟨G, J⟩
 
+/-- A subset together with the remaining part reconstructs the larger set. -/
+theorem subset_union_diff {s₁ s₂ : S} (H : s₁ ⊆ s₂) : s₁ ∪ (s₂ \ s₁) = s₂ := by
+  rw [union_comm]
+  exact (diff_subset_decomp H).symm
+
 /-- De Morgan's law: difference distributes over union. -/
 theorem diff_union {s₁ s₂ s₃ : S} : s₁ \ (s₂ ∪ s₃) = (s₁ \ s₂) ∩ (s₁ \ s₃) := by
   ext x; rw [mem_diff, mem_union, mem_inter, mem_diff, mem_diff]

From 18c469f3bcaa5f83b08bbf9edf9ca71685d570ea Mon Sep 17 00:00:00 2001
From: HaleOIC <yunsongyang730@gmail.com>
Date: Thu, 9 Apr 2026 11:29:39 +0200
Subject: [PATCH 6/7] Improve fancy update mask mismatch errors

---
 src/Iris/ProofMode/Classes.lean          |  6 ++++--
 src/Iris/ProofMode/InstancesUpdates.lean | 12 ++++++++++++
 src/Iris/ProofMode/Tactics/Basic.lean    | 11 ++++++++---
 src/Iris/Tests/Tactics.lean              | 18 ++++++++++++++++++
 4 files changed, 42 insertions(+), 5 deletions(-)

diff --git a/src/Iris/ProofMode/Classes.lean b/src/Iris/ProofMode/Classes.lean
index 4d3c4cbb..b8a46471 100644
--- a/src/Iris/ProofMode/Classes.lean
+++ b/src/Iris/ProofMode/Classes.lean
@@ -14,6 +14,10 @@ public import Iris.ProofMode.Modalities
 namespace Iris.ProofMode
 open Iris.BI
 
+/-- [PMError] is used as precondition on "failing" instances of typeclasses
+  that have pure preconditions (such as [ElimModal]) -/
+inductive PMError (msg : String) : Prop
+
 /-- [InOut] is used to dynamically determine whether a type class
 parameter is an input or an output. This is important for classes that
 are used with multiple modings, e.g., IntoWand. Instances can match on
@@ -36,7 +40,6 @@ theorem asEmpValid_1 [BI PROP] (P : PROP) [AsEmpValid .into φ P] : φ → ⊢ P
 theorem asEmpValid_2 [BI PROP] (φ : Prop) [AsEmpValid .from φ (P : PROP)] : (⊢ P) → φ :=
   AsEmpValid.as_emp_valid.2 rfl
 
-
 /- Depending on the use case, type classes with the prefix `From` or `Into` are used. Type classes
 with the prefix `From` are used to generate one or more propositions *from* which the original
 proposition can be derived. Type classes with the prefix `Into` are used to generate propositions
@@ -126,7 +129,6 @@ class IntoAbsorbingly [BI PROP] (P : outParam PROP) (Q : PROP) where
   into_absorbingly : P ⊢ <absorb> Q
 export IntoAbsorbingly (into_absorbingly)
 
-
 @[ipm_class]
 class FromAssumption (p : Bool) [BI PROP] (ioP : InOut) (P : semiOutParam PROP) (Q : PROP) where
   from_assumption : □?p P ⊢ Q
diff --git a/src/Iris/ProofMode/InstancesUpdates.lean b/src/Iris/ProofMode/InstancesUpdates.lean
index 871a6d5e..a6ed4137 100644
--- a/src/Iris/ProofMode/InstancesUpdates.lean
+++ b/src/Iris/ProofMode/InstancesUpdates.lean
@@ -146,12 +146,24 @@ instance fromModal_fupd E (P : PROP) :
     FromModal True modality_id iprop(|={E}=> P) iprop(|={E}=> P) P where
   from_modal := by simp [modality_id]; exact fupd_intro
 
+instance (priority := low) fromModal_fupd_wrongMask E1 E2 (P : PROP) :
+    FromModal (PMError "Only non-mask-changing update modalities can be introduced directly.
+      Use `iapply (fupd_mask_intro ...)` to introduce a mask-changing fancy update.")
+      modality_id iprop(|={E1,E2}=> P) iprop(|={E1,E2}=> P) P where
+  from_modal h := by cases h
+
 instance elimModal_bupd_fupd p E1 E2 (P Q : PROP) :
     ElimModal True p false iprop(|==> P) P iprop(|={E1,E2}=> Q) iprop(|={E1,E2}=> Q) where
   elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans <|
     (sep_mono_l BIUpdateFUpdate.fupd_of_bupd).trans <|
     fupd_frame_r.trans <| (BIFUpdate.mono wand_elim_r).trans BIFUpdate.trans
 
+instance (priority := low) elimModal_fupd_fupd_wrongMask p E0 E1 E2 E3 (P Q : PROP) :
+    ElimModal (PMError "Goal and eliminated modality must have the same mask.
+      Use `BIFUpdate.subset` to adjust the goal mask before using `imod`.")
+      p false iprop(|={E1,E2}=> P) iprop(False) iprop(|={E0,E3}=> Q) iprop(False) where
+  elim_modal h := by cases h
+
 instance (priority := high) elimModal_fupd_fupd p E1 E2 E3 (P Q : PROP) :
     ElimModal True p false iprop(|={E1,E2}=> P) P iprop(|={E1,E3}=> Q) iprop(|={E2,E3}=> Q) where
   elim_modal _ := (sep_mono_l intuitionisticallyIf_elim).trans <|
diff --git a/src/Iris/ProofMode/Tactics/Basic.lean b/src/Iris/ProofMode/Tactics/Basic.lean
index 9c050f9a..3f2d23d9 100644
--- a/src/Iris/ProofMode/Tactics/Basic.lean
+++ b/src/Iris/ProofMode/Tactics/Basic.lean
@@ -16,9 +16,14 @@ namespace Iris.ProofMode
 open Lean Elab.Tactic Meta Qq BI Std
 
 def iSolveSideconditionAt (m : MVarId) : ProofModeM Unit := do
-  let gs ← evalTacticAt (← `(tactic | trivial)) m
-  if !gs.isEmpty then
-    throwError "isolvesidecondition: failed to solve sidecondition {← m.getType}"
+  let goal ← instantiateMVars (← m.getType)
+  match goal with
+  | .app (.const ``PMError _) (.lit (.strVal msg)) =>
+      throwError "{msg}"
+  | _ =>
+      let gs ← evalTacticAt (← `(tactic | trivial)) m
+      if !gs.isEmpty then
+        throwError "isolvesidecondition: failed to solve sidecondition {goal}"
 
 elab "istart" : tactic => do
   let (mvar, _) ← startProofMode (← getMainGoal)
diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean
index 5868136d..6a383681 100644
--- a/src/Iris/Tests/Tactics.lean
+++ b/src/Iris/Tests/Tactics.lean
@@ -1664,6 +1664,15 @@ example [BI PROP] [BIFUpdate PROP]
   imodintro
   iexact HP
 
+/- Tests `imodintro` for mask-changing fupd failing -/
+/-- error: Only non-mask-changing update modalities can be introduced directly.
+      Use `iapply (fupd_mask_intro ...)` to introduce a mask-changing fancy update. -/
+#guard_msgs in
+example [BI PROP] [BIFUpdate PROP]
+    (E1 E2 : CoPset) (P : PROP) : P ⊢ |={E1,E2}=> P := by
+  iintro HP
+  imodintro
+
 /-- Tests `imodintro` for bupd preserves both intuitionistic and spatial -/
 example [BI PROP] [BIUpdate PROP] (P Q : PROP) : □ P ∗ Q ⊢ |==> Q := by
   iintro ⟨#HP, HQ⟩
@@ -1756,6 +1765,15 @@ example [BI PROP] [BIFUpdate PROP]
   imodintro
   iexact HP
 
+/- Tests `imod` for fupd with mismatching masks failing -/
+/-- error: Goal and eliminated modality must have the same mask.
+      Use `BIFUpdate.subset` to adjust the goal mask before using `imod`. -/
+#guard_msgs in
+example [BI PROP] [BIFUpdate PROP]
+    (E0 E1 E2 E3 : CoPset) (P Q : PROP) : (|={E1,E2}=> P) ⊢ |={E0,E3}=> Q := by
+  iintro HP
+  imod HP
+
 /-- Tests `imod` removing later before timeless propositions -/
 example [BI PROP] [BIUpdate PROP] (P : PROP) [Timeless P] : ▷ P ⊢ ◇ P := by
   iintro HP

From 1387fa817581c6ac44763af5bcb8a75ef6547906 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 9 Apr 2026 12:08:58 +0200
Subject: [PATCH 7/7] minimal tweak

---
 src/Iris/BI/Updates.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Iris/BI/Updates.lean b/src/Iris/BI/Updates.lean
index e91a08ab..4171128f 100644
--- a/src/Iris/BI/Updates.lean
+++ b/src/Iris/BI/Updates.lean
@@ -287,7 +287,7 @@ theorem fupd_mask_frame_acc {E E' E1 E2 : CoPset} {P Q : PROP}:
   exact emp_sep.1.trans <| (fupd_mask_frame_r hdisj).trans <| by simp [subset_union_diff hE]
 
 theorem fupd_mask_subseteq_emptyset_difference {E1 E2 : CoPset} :
-    E2 ⊆ E1 → ⊢ |={E1,E2}=> |={∅,E1\E2}=> (emp: PROP) :=
+    E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={∅,E1\E2}=> emp :=
   λ h => by
     simpa [union_comm, subset_union_diff h] using (fupd_mask_intro_subseteq empty_subset).trans <|
       fupd_mask_frame_r (P := iprop(|={∅,E1 \ E2}=> (emp : PROP))) (disjoint_symm <| disjoint_diff_right)