diff --git a/Iris/Iris/Algebra/IProp.lean b/Iris/Iris/Algebra/IProp.lean
index 13c34a4e0..17ca2f5b1 100644
--- a/Iris/Iris/Algebra/IProp.lean
+++ b/Iris/Iris/Algebra/IProp.lean
@@ -20,39 +20,65 @@ open COFE
 
 abbrev GType := Nat
 
-def BundledGFunctors := GType → Σ F : OFunctorPre, RFunctorContractive F
+@[rocq_alias gFunctor]
+abbrev GFunctor := Σ F : OFunctorPre, RFunctorContractive F
+
+@[rocq_alias gFunctors]
+def BundledGFunctors := GType → GFunctor
 
 def BundledGFunctors.default : BundledGFunctors := fun _ => ⟨constOF Unit, by infer_instance⟩
 
-def BundledGFunctors.set (GF : BundledGFunctors) (i : Nat) (FB : Σ F, RFunctorContractive F) :
+def BundledGFunctors.set (GF : BundledGFunctors) (i : Nat) (FB : GFunctor) :
     BundledGFunctors :=
   fun j => if j = i then FB else GF j
 
+#rocq_ignore gid "Use `GType` (= `Nat`) to index `BundledGFunctors` directly."
+#rocq_ignore gFunctors.nil "`BundledGFunctors` is a function `GType → GFunctor`; no list combinators."
+#rocq_ignore gFunctors.singleton "`BundledGFunctors` is a function `GType → GFunctor`; no list combinators."
+#rocq_ignore gFunctors.app "`BundledGFunctors` is a function `GType → GFunctor`; no list combinators."
+
+@[rocq_alias gname]
 abbrev GName := Nat
 
+#rocq_ignore gnameO "Use `LeibnizO GName`."
+
+@[rocq_alias iResF]
 abbrev IResF (GF : BundledGFunctors) : OFunctorPre :=
   DiscreteFunOF (fun i => GenMapOF (GF i).fst)
 
+#rocq_ignore subG "Superseded by `ElemG`."
+#rocq_ignore subG_inv "Lemma about `subG`; obsolete with `ElemG`."
+#rocq_ignore subG_refl "Lemma about `subG`; obsolete with `ElemG`."
+#rocq_ignore subG_app_l "Lemma about `subG`; obsolete with `ElemG`."
+#rocq_ignore subG_app_r "Lemma about `subG`; obsolete with `ElemG`."
+
 instance (GF : BundledGFunctors) (i : GName) : RFunctorContractive ((GF i).fst) := (GF i).snd
 
 section IProp
 
 variable (GF : BundledGFunctors)
 
+@[rocq_alias iProp_solution.iPrePropO, rocq_alias iProp_solution.iProp_result]
 def IPre : Type _ := OFunctor.Fix (UPredOF (IResF GF))
 
+@[rocq_alias iProp_solution.iPreProp_cofe]
 instance : COFE (IPre GF) := inferInstanceAs (COFE (OFunctor.Fix _))
 
+@[rocq_alias iProp_solution.iResUR]
 def IResUR : Type := (i : GType) → GenMap (GF i |>.fst (IPre GF) (IPre GF))
 
+#rocq_ignore iResUR "Sealed copy of `iProp_solution.iResUR`; not needed since Lean does not seal it."
+
 instance : UCMRA (IResUR GF) :=
   ucmraDiscreteFunO (β := fun (i : GType) => GenMap (GF i |>.fst (IPre GF) (IPre GF)))
 
 abbrev IProp := UPred (IResUR GF)
 
+@[rocq_alias iProp_solution.iProp_unfold]
 def IProp.unfold : IProp GF -n> IPre GF :=
   OFE.Iso.hom <| OFunctor.Fix.iso (F := (UPredOF (IResF GF)))
 
+@[rocq_alias iProp_solution.iProp_fold]
 def IProp.fold : IPre GF -n> IProp GF :=
   OFE.Iso.inv <| OFunctor.Fix.iso (F := (UPredOF (IResF GF)))
 
diff --git a/Iris/Iris/Algebra/UPred.lean b/Iris/Iris/Algebra/UPred.lean
index 05789e738..ea15cf771 100644
--- a/Iris/Iris/Algebra/UPred.lean
+++ b/Iris/Iris/Algebra/UPred.lean
@@ -35,7 +35,7 @@ theorem ValidAt.le_rfl {M : Type _} [UCMRA M] {n : Nat} {Hle : n ≤ n} {v : Val
   v.le Hle = v := by rfl
 
 /-- The data of a UPred object is an indexed proposition over M (Bundled version) -/
-@[ext]
+@[ext, rocq_alias uPred]
 structure UPred (M : Type _) [UCMRA M] where
   holds : (n : Nat) → ValidAt M n → Prop
   mono {n1 n2} {x1 : ValidAt M n1} {x2 : ValidAt M n2} :
@@ -62,6 +62,7 @@ variable [UCMRA M]
 
 open UPred
 
+@[rocq_alias uPredO]
 instance : OFE (UPred M) where
   Equiv P Q := ∀ n (x : M), (p : ✓{n} x) → (P n ⟨x, p⟩ ↔ Q n ⟨x, p⟩)
   Dist n P Q := ∀ n' (x : M), n' ≤ n → (p : ✓{n'} x) → (P n' ⟨x, p⟩ ↔ Q n' ⟨x, p⟩)
@@ -75,21 +76,32 @@ instance : OFE (UPred M) where
   dist_lt Hdist Hlt _ _ Hle Hvalid :=
     Hdist _ _ (Nat.le_trans Hle (Nat.le_of_succ_le Hlt)) Hvalid
 
+#rocq_ignore uPred_equiv' "Inlined in the `OFE` construction"
+#rocq_ignore uPred_equiv "Not needed"
+#rocq_ignore uPred_dist' "Inlined in the `OFE` construction"
+#rocq_ignore uPred_dist "Not needed"
+#rocq_ignore uPred_ofe_mixin "Not needed"
+
+
 instance : OFE.Leibniz (UPred M) where
   eq_of_eqv {x y} hequiv := by
     ext n e
     exact hequiv n e.val e.property
 
+@[rocq_alias uPred_ne]
 theorem uPred_ne {P : UPred M} {n} {m₁ m₂ : ValidAt M n} (H : (m₁ : M) ≡{n}≡ (m₂ : M)) : P n m₁ ↔ P n m₂ :=
   ⟨fun H' => P.mono H' H.to_incN .refl, fun H' => P.mono H' H.symm.to_incN .refl⟩
 
+@[rocq_alias uPred_proper]
 theorem uPred_proper {P : UPred M} {n} {m₁ m₂ : ValidAt M n} (H : (m₁ : M) ≡ (m₂ : M)) : P n m₁ ↔ P n m₂ :=
   uPred_ne H.dist
 
+@[rocq_alias uPred_holds_ne]
 theorem uPred_holds_ne {P Q : UPred M} {n₁ n₂} {x : M}
     (HPQ : P ≡{n₂}≡ Q) (Hn : n₂ ≤ n₁) (Hx : ✓{n₂} x) (Hx' : ✓{n₁} x) (HQ : Q n₁ ⟨x, Hx'⟩) : P n₂ ⟨x, Hx⟩ :=
   (HPQ _ _ .refl Hx).mpr (Q.mono HQ .rfl Hn)
 
+@[rocq_alias uPred_cofe]
 instance : IsCOFE (UPred M) where
   compl c := {
     holds n x := ∀ n', (Hle : n' ≤ n) → (c n') n' (x.le Hle)
@@ -102,9 +114,12 @@ instance : IsCOFE (UPred M) where
     refine ⟨fun H => H _ .refl, fun H n' Hn' => ?_⟩
     exact (c.cauchy Hn' _ _ .refl _).mp (mono _ H .rfl Hn')
 
+#rocq_ignore uPred_compl "Inlined in the `IsCOFE` construction"
+
 abbrev UPredOF (F : COFE.OFunctorPre) [URFunctor F] : COFE.OFunctorPre :=
   fun A B _ _ => UPred (F B A)
 
+@[rocq_alias uPredO_map]
 def uPred_map [UCMRA α] [UCMRA β] (f : β -C> α) : UPred α -n> UPred β := by
   refine ⟨fun P => ⟨fun n x => P n ⟨(f x.val), f.validN x.property⟩, ?_⟩, ⟨?_⟩⟩
   · intro n1 n2 x1 x2 HP Hm Hn
@@ -112,6 +127,9 @@ def uPred_map [UCMRA α] [UCMRA β] (f : β -C> α) : UPred α -n> UPred β := b
   · intro n x1 x2 Hx1x2 n' y Hn' Hv
     exact Hx1x2 _ _ Hn' (f.validN Hv)
 
+#rocq_ignore uPred_map "Inlined in `uPred_map`"
+
+@[rocq_alias uPredOF]
 instance [URFunctor F] : COFE.OFunctor (UPredOF F) where
   cofe := inferInstance
   map f g := uPred_map (URFunctor.map (F := F) g f)
@@ -125,6 +143,7 @@ instance [URFunctor F] : COFE.OFunctor (UPredOF F) where
     simp only [uPred_map]
     exact uPred_proper <| URFunctor.map_comp g' f' g f H
 
+@[rocq_alias uPredOF_contractive]
 instance instUPredOFunctorContractive [URFunctorContractive F] : COFE.OFunctorContractive (UPredOF F) where
   map_contractive.1 {n x y} HKL P m a Hmn Ha := by
     refine uPred_ne (P := P) <|
diff --git a/Iris/Iris/BI/Plainly.lean b/Iris/Iris/BI/Plainly.lean
index f276a1023..af8650572 100644
--- a/Iris/Iris/BI/Plainly.lean
+++ b/Iris/Iris/BI/Plainly.lean
@@ -682,6 +682,11 @@ theorem prop_ext (P Q : PROP) : iprop(internalEq P Q ⊣⊢ ■ (P ∗-∗ Q)) :
   have ⟨mp, mpr⟩:= prop_ext_siEmpValid_equiv P Q
   ⟨siPure_mono mp, siPure_mono mpr⟩
 
+#rocq_ignore prop_ext_2 "Subsumed by `prop_ext_symm`"
+
+theorem prop_ext_symm (P Q : PROP) : iprop(■ (P ∗-∗ Q) ⊣⊢ internalEq P Q) :=
+  prop_ext P Q |>.symm
+
 @[rocq_alias plainly_alt]
 theorem plainly_alt (P : PROP) : ■ P ⊣⊢ internalEq iprop(<affine> P) iprop(emp) := by
   apply plainly_affinely_elim.symm.trans
diff --git a/Iris/Iris/BI/Sbi.lean b/Iris/Iris/BI/Sbi.lean
index 603428670..669b3882b 100644
--- a/Iris/Iris/BI/Sbi.lean
+++ b/Iris/Iris/BI/Sbi.lean
@@ -335,7 +335,6 @@ theorem siEmpValid_exist_mpr [Sbi PROP] {A : Type _} {Φ : A → PROP} :
     (∃ x, <si_emp_valid> Φ x) ⊢@{SiProp} <si_emp_valid> (∃ x, Φ x) :=
   exists_elim fun x => siEmpValid_mono (exists_intro x)
 
-@[rocq_alias uPred_primitive.si_emp_valid_exist_1]
 theorem siEmpValid_exist_mp [Sbi PROP] [SbiEmpValidExist PROP] {A : Type _} {Φ : A → PROP} :
     <si_emp_valid> (∃ x, Φ x) ⊢@{SiProp} ∃ x, <si_emp_valid> Φ x :=
   calc iprop(<si_emp_valid> (∃ x, Φ x))
diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean
index 18729626e..2cbe9782c 100644
--- a/Iris/Iris/Instances/IProp/Instance.lean
+++ b/Iris/Iris/Instances/IProp/Instance.lean
@@ -58,10 +58,14 @@ end TranspAp
 
 section ElemG
 
+/-- `ElemG` takes functors instead of CMRAs -/
+@[rocq_alias inG]
 class ElemG (FF : BundledGFunctors) (F : OFunctorPre) [RFunctorContractive F] where
   τ : GType
   transp : FF τ = ⟨F, ‹_›⟩
 
+#rocq_ignore subG_inG "Superseded by Lean's direct `ElemG` typeclass synthesis."
+
 open OFE
 
 variable [I : RFunctorContractive F]
@@ -69,7 +73,7 @@ variable [I : RFunctorContractive F]
 def ElemG.transpMap (E : ElemG GF F) T [OFE T] : (GF E.τ).fst = F :=
   Sigma.mk.inj E.transp |>.1
 
-def ElemG.transpClass (E : ElemG GF F) T [OFE T] : HEq (GF E.τ).snd I :=
+def ElemG.transpClass (E : ElemG GF F) T [OFE T] : (GF E.τ).snd ≍ I :=
   Sigma.mk.inj E.transp |>.2
 
 def ElemG.bundle (E : ElemG GF F) [OFE T] : F.ap T → GF.api E.τ T :=
@@ -114,10 +118,10 @@ theorem bundle_op {GF : BundledGFunctors} [E : ElemG GF F] (a2 ac : F.ap (IProp
 
 theorem unbundle_op {GF : BundledGFunctors} [E : ElemG GF F] (a2 ac : GF.api (ElemG.τ GF F) (IProp GF)) :
   E.unbundle (a2 • ac) ≡ E.unbundle a2 • E.unbundle ac :=
-  OFE.transpAp_op_mp (E.transpMap ((GF (ElemG.τ GF F)).fst.ap (IPre GF))) (E.transpClass ((GF (ElemG.τ GF F)).fst.ap (IPre GF)))
+  OFE.transpAp_op_mp (E.transpMap ((GF (ElemG.τ GF F)).fst.ap (IPre GF)))
+    (E.transpClass ((GF (ElemG.τ GF F)).fst.ap (IPre GF)))
 
-theorem ElemG.bundle_unit {GF F} [RFunctorContractive F] (E : ElemG GF F)
-    {ε : F.ap (IProp GF)} [IsUnit ε] :
+theorem ElemG.bundle_unit {GF F} [RFunctorContractive F] (E : ElemG GF F) {ε : F.ap (IProp GF)} [IsUnit ε] :
     IsUnit (E.bundle ε) := by
   refine { unit_valid := ?_, unit_left_id := ?_, pcore_unit := ?_ }
   · refine CMRA.valid_iff_validN.mpr fun n => ?_
@@ -155,18 +159,22 @@ open Iris COFE UPred
 variable {FF : BundledGFunctors}
 
 /-- Isorecursive unfolding for each projection of FF. -/
+@[rocq_alias inG_unfold]
 def IProp.unfoldi : FF.api τ (IProp FF) -n> FF.api τ (IPre FF) :=
   OFunctor.map (IProp.fold FF) (IProp.unfold FF)
 
 /-- Isorecursive folding for each projection of FF. -/
+@[rocq_alias inG_fold]
 def IProp.foldi : FF.api τ (IPre FF) -n> FF.api τ (IProp FF) :=
   OFunctor.map (IProp.unfold FF) (IProp.fold FF)
 
+@[rocq_alias inG_unfold_fold]
 theorem IProp.unfoldi_foldi (x : FF.api τ (IPre FF)) : unfoldi (foldi x) ≡ x := by
   refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm ?_
   refine .trans ?_ (OFunctor.map_id (F := FF τ |>.fst) x)
   apply OFunctor.map_ne.eqv <;> intro _ <;> simp [IProp.unfold, IProp.fold]
 
+@[rocq_alias inG_fold_unfold]
 theorem IProp.foldi_unfoldi (x : FF.api τ (IProp FF)) : foldi (unfoldi x) ≡ x := by
   refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm ?_
   refine .trans ?_ (OFunctor.map_id (F := FF τ |>.fst) x)
@@ -189,10 +197,14 @@ theorem IProp.unfoldi_validN {n : Nat} (x : FF.api τ (IProp FF)) (H : ✓{n} x)
 theorem IProp.validN_foldi {n : Nat} (x : FF.api τ (IPre FF)) (H : ✓{n} (foldi x)) : ✓{n} x :=
   CMRA.validN_ne (IProp.unfoldi_foldi x).dist (IProp.unfoldi_validN _ H)
 
-theorem IProp.validN_unfoldi {n : Nat} (x : FF.api τ (IProp FF)) (H : ✓{n} (unfoldi x)) : ✓{n} x :=
+theorem IProp.validN_unfoldi_mp {n : Nat} (x : FF.api τ (IProp FF)) (H : ✓{n} (unfoldi x)) : ✓{n} x :=
   CMRA.validN_ne (IProp.foldi_unfoldi x).dist (IProp.foldi_validN _ H)
 
--- unfoldi preserves unit structure
+@[rocq_alias inG_unfold_validN]
+theorem IProp.validN_unfoldi {n : Nat} (x : FF.api τ (IProp FF)) : ✓{n} (unfoldi x) ↔ ✓{n} x :=
+  ⟨IProp.validN_unfoldi_mp x,IProp.unfoldi_validN x⟩
+
+/-- unfoldi preserves unit structure -/
 theorem IProp.unfoldi_unit {τ : GType} {x : FF.api τ (IProp FF)} [IsUnit x] :
     IsUnit (unfoldi x) := by
   refine { unit_valid := ?_, unit_left_id := ?_, pcore_unit := ?_ }
@@ -459,6 +471,9 @@ end iSingleton
 def iOwn {GF F} [RFunctorContractive F] [E : ElemG GF F] (γ : GName) (v : F.ap (IProp GF)) : IProp GF :=
   UPred.ownM <| iSingleton F γ v
 
+#rocq_ignore own_def "`iOwn` is defined directly without `seal`/`unseal`."
+#rocq_ignore own_aux "`iOwn` is defined directly without `seal`/`unseal`."
+
 section iOwn
 
 open IProp OFE UPred BI GenMap
@@ -617,7 +632,6 @@ theorem iOwn_alloc_strong_dep (f : GName → F.ap (IProp GF)) (P : GName → Pro
     subst Hm
     exact BI.exists_intro' γ (BI.persistent_entails_r (BI.pure_intro HPγ))
 
-
 private theorem list_not_mem_of_gt_max (G : List Nat) (k : Nat) (hk : G.foldr max 0 < k) :
     k ∉ G := by
   intro hmem
diff --git a/Iris/Iris/Instances/Lib/FUpd.lean b/Iris/Iris/Instances/Lib/FUpd.lean
index 851325b16..8aa61eae6 100644
--- a/Iris/Iris/Instances/Lib/FUpd.lean
+++ b/Iris/Iris/Instances/Lib/FUpd.lean
@@ -22,6 +22,10 @@ open Iris OFE COFE BI Auth
 
 section InvG
 
+@[rocq_alias has_lc]
+abbrev hasLc := Bool
+
+@[rocq_alias invGpreS]
 class InvGpreS (GF : BundledGFunctors) where
   toWsatGpreS : WsatGpreS GF
   toLcGpreS : LcGpreS GF
@@ -29,7 +33,8 @@ class InvGpreS (GF : BundledGFunctors) where
 attribute [reducible, instance] InvGpreS.toWsatGpreS
 attribute [reducible, instance] InvGpreS.toLcGpreS
 
-class InvGS_gen (hlc : outParam Bool) (GF : BundledGFunctors) extends InvGpreS GF where
+@[rocq_alias invGS_gen]
+class InvGS_gen (hlc : outParam hasLc) (GF : BundledGFunctors) extends InvGpreS GF where
   toWsatGS : WsatGS GF
   toLcGS : LcGS GF
 
@@ -38,12 +43,20 @@ attribute [reducible, instance] InvGS_gen.toLcGS
 
 abbrev InvGS := InvGS_gen true
 
+#rocq_ignore «invΣ» "Superseded by the `InvGpreS` typeclass on `BundledGFunctors`."
+#rocq_ignore «subG_invΣ» "Superseded by Lean's direct `ElemG` typeclass synthesis."
+
 end InvG
 
 section FUpd
 
 variable {GF : BundledGFunctors} {hlc : Bool} [InvGS_gen hlc GF]
 
+#rocq_ignore uPred_fupd_def "`uPred_fupd` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_fupd_aux "`uPred_fupd` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_fupd_unseal "`uPred_fupd` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias uPred_fupd]
 def uPred_fupd (E1 E2 : CoPset) (P : IProp GF) : IProp GF :=
   iprop(wsat ∗ ownE E1 -∗ le_upd_if hlc iprop(◇ (wsat ∗ ownE E2 ∗ P)))
 
@@ -65,6 +78,8 @@ section Instances
 
 open Std.LawfulSet
 
+#rocq_ignore uPred_fupd_mixin "The `BiFUpdMixin` laws are supplied directly when building `uPred_bi_fupd` below."
+
 @[rocq_alias uPred_bi_fupd]
 instance uPred_bi_fupd {GF : BundledGFunctors} [InvGS_gen hlc GF] : BIFUpdate (IProp GF) where
   fupd := uPred_fupd
@@ -224,6 +239,8 @@ theorem fupd_soundness_lc [InvGpreS GF] {E1 E2 : CoPset} {P : IProp GF} [Plain P
   iapply le_upd_later $$ Hcr [H]
   iapply except0_into_later $$ H
 
+#rocq_ignore fupd_soundness_no_lc_unfold "Proof inlined in fupd_soundness_no_lc"
+
 @[rocq_alias fupd_soundness_no_lc]
 theorem fupd_soundness_no_lc [InvGpreS GF] {E1 E2 : CoPset} {P : IProp GF} [Plain P]
     (H : ∀ (_ : InvGS_gen false GF), ⊢ £ m -∗ |={E1,E2}=> P) : ⊢ P := by
diff --git a/Iris/Iris/Instances/Lib/Invariants.lean b/Iris/Iris/Instances/Lib/Invariants.lean
index 76e632fc5..c9f397bdd 100644
--- a/Iris/Iris/Instances/Lib/Invariants.lean
+++ b/Iris/Iris/Instances/Lib/Invariants.lean
@@ -15,9 +15,7 @@ import Iris.Instances.Lib.WSat
 
 @[expose] public section
 
-/-! ## Invariants
-TODO: into_inv_inv, into_acc_inv
--/
+/-! ## Invariants -/
 
 namespace Iris
 
@@ -27,9 +25,15 @@ section InvariantDefinition
 
 variable {GF : BundledGFunctors} [InvGS_gen hlc GF]
 
+#rocq_ignore inv_def "`inv` is defined directly without `seal`/`unseal`."
+#rocq_ignore inv_aux "`inv` is defined directly without `seal`/`unseal`."
+#rocq_ignore inv_unseal "`inv` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias inv]
 def inv (N : Namespace) (P : IProp GF) : IProp GF :=
   iprop(□ ∀ E, ⌜↑N ⊆ E⌝ → |={E, E \ ↑N}=> ▷ P ∗ (▷ P ={E \ ↑N, E}=∗ True))
 
+@[rocq_alias own_inv]
 def own_inv (N : Namespace) (P : IProp GF) : IProp GF :=
   iprop(∃ i, ⌜i ∈ (↑N : CoPset)⌝ ∧ ownI i P)
 
@@ -84,6 +88,8 @@ theorem except_0_inv (N : Namespace) (P : IProp GF) : ⊢ ◇ inv N P -∗ inv N
 instance is_except_0_inv (N : Namespace) (P : IProp GF) : IsExcept0 (inv N P) where
   is_except0 := by iintro H; iapply except_0_inv $$ H
 
+-- TODO: into_inv_inv, into_acc_inv
+
 end Instances
 
 section BasicLemmas
diff --git a/Iris/Iris/Instances/Lib/LaterCredits.lean b/Iris/Iris/Instances/Lib/LaterCredits.lean
index cf4edbbdb..5816ebe81 100644
--- a/Iris/Iris/Instances/Lib/LaterCredits.lean
+++ b/Iris/Iris/Instances/Lib/LaterCredits.lean
@@ -13,9 +13,7 @@ public import Iris.Instances.IProp
 
 @[expose] public section
 
-/-! ## Later credits
-TODO: missing instances for PM: combine_sep_lc_add, combine_sep_lc_S_l
--/
+/-! ## Later credits -/
 
 namespace Iris
 
@@ -40,25 +38,40 @@ scoped instance : CMRA.Discrete Credit := CommMonoidLike.instDiscrete
 scoped instance {a : Credit} : CMRA.Cancelable a := inferInstance
 
 /-- Later credits inclusion typeclass (`GF` contains the necessary functors for later credits) -/
+@[rocq_alias lcGpreS]
 class LcGpreS (GF : BundledGFunctors) where
   lc_elem : ElemG GF (AuthURF (F := PNat) (constOF Credit))
 
 attribute [reducible, instance] LcGpreS.lc_elem
 
+@[rocq_alias lcGS]
 class LcGS (GF : BundledGFunctors) extends LcGpreS GF where
   lc_name : GName
 
+#rocq_ignore «lcΣ» "Superseded by the `LcGpreS` typeclass on `BundledGFunctors`."
+#rocq_ignore «subG_lcΣ» "Superseded by Lean's direct `ElemG` typeclass synthesis."
+
 end LcGS
 
 section Definitions
 
 variable {GF : BundledGFunctors} [LC : LcGS GF]
 
+#rocq_ignore lc_def "`lc` is defined directly without `seal`/`unseal`."
+#rocq_ignore lc_aux "`lc` is defined directly without `seal`/`unseal`."
+#rocq_ignore lc_unseal "`lc` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias lc]
 def lc (i : Credit) : IProp GF :=
   iOwn (E := LC.lc_elem) LC.lc_name (◯ i)
 
 notation:max "£ " i:40 => lc i
 
+#rocq_ignore lc_supply_def "`lc_supply` is defined directly without `seal`/`unseal`."
+#rocq_ignore lc_supply_aux "`lc_supply` is defined directly without `seal`/`unseal`."
+#rocq_ignore lc_supply_unseal "`lc_supply` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias lc_supply]
 def lc_supply (i : Credit) : IProp GF :=
   iOwn (E := LC.lc_elem) LC.lc_name (● i)
 
@@ -68,6 +81,7 @@ section Operations
 
 variable {GF : BundledGFunctors} [LC : LcGS GF]
 
+@[rocq_alias lc_split]
 theorem lc_split {n m} : £ (n + m) ⊣⊢@{IProp GF} £ n ∗ £ m := by
   -- FIXME: Timeout on iOwn_op. Why?
   refine .trans ?_ iOwn_op
@@ -139,6 +153,8 @@ instance (priority := default - 10) {n m} : FromSep (PROP := IProp GF) (£ (n +
 instance (priority := default) {n} : FromSep (PROP := IProp GF) (£ (.succ n)) (£ 1) (£ n) where
   from_sep := lc_succ.mpr
 
+-- TODO: combine_sep_lc_add, combine_sep_lc_S_l
+
 @[rocq_alias into_sep_lc_add]
 instance (priority := default - 10) {n m} : IntoSep (PROP := IProp GF) (£ (n + m)) (£ n) (£ m) where
   into_sep := lc_split.mp
@@ -173,6 +189,10 @@ instance {P : IProp GF} : Contractive (le_upd_pre P) where
     · exact distLater_zero
     · exact distLater_succ.mpr (distLater_succ.mp H)
 
+#rocq_ignore le_upd.le_upd_def "`le_upd` is defined directly without `seal`/`unseal`."
+#rocq_ignore le_upd.le_upd_aux "`le_upd` is defined directly without `seal`/`unseal`."
+#rocq_ignore le_upd.le_upd_unseal "`le_upd` is defined directly without `seal`/`unseal`."
+
 @[rocq_alias le_upd.le_upd]
 def le_upd (P : IProp GF) : IProp GF := fixpoint (le_upd_pre P)
 
@@ -316,6 +336,8 @@ theorem except_0_le_upd {P : IProp GF} : ◇ (|==£> P) ⊢ |==£> (◇ P) := by
     iright
     iexact H
 
+#rocq_ignore le_upd.bi_bupd_mixin_le_upd "Only a safety check, not used"
+
 end Upd
 
 section Internal
@@ -498,7 +520,7 @@ def le_upd_if (b : Bool) : IProp GF → IProp GF :=
 instance le_upd_if_ne : NonExpansive (le_upd_if b (GF := GF)) := by
   cases b <;> (simp only [le_upd_if, Bool.false_eq_true, ↓reduceIte]; infer_instance)
 
-@[rocq_alias le_upd_if.le_upd_if_mono']
+@[rocq_alias le_upd_if.le_upd_if_mono]
 theorem le_upd_if_mono {P Q : IProp GF} : (P ⊢ Q) → (le_upd_if b P) ⊢ (le_upd_if b Q) := by
   cases b <;> (simp only [le_upd_if, Bool.false_eq_true, ↓reduceIte])
   · intro H; iintro G
@@ -554,6 +576,10 @@ theorem except_0_le_upd_if {b} {P : IProp GF} : ◇ (le_upd_if b P) ⊢ le_upd_i
 instance {b} {p} {P Q : IProp GF} : ElimModal True p false (bupd P) P (le_upd_if b Q) (le_upd_if b Q) := by
   cases b <;> (simp only [le_upd_if, Bool.false_eq_true, ↓reduceIte]; infer_instance)
 
+@[rocq_alias le_upd_if.from_assumption_le_upd_if]
+instance from_assumption_le_upd_if {p} {P Q : IProp GF} [h : FromAssumption p ioP P Q] : FromAssumption p ioP P (le_upd_if b Q) where
+  from_assumption := h.1.trans le_upd_if_intro
+
 @[rocq_alias le_upd_if.from_pure_le_upd_if]
 instance {b} {a} {P : IProp GF} φ [FromPure a P io φ] : FromPure a (le_upd_if b P) io φ := by
   cases b <;> (simp only [le_upd_if, Bool.false_eq_true, ↓reduceIte]; infer_instance)
@@ -575,10 +601,6 @@ instance {b} {p} {P Q : IProp GF} :
 instance {p b} {P R Q : IProp GF} [hf : Frame p R P Q] : Frame p R (le_upd_if b P) (le_upd_if b Q) where
   frame := le_upd_if_frame_l.trans <| le_upd_if_mono hf.frame
 
-@[rocq_alias le_upd_if.from_assumption_le_upd_if]
-instance from_assumption_le_upd_if {p} {P Q : IProp GF} [h : FromAssumption p ioP P Q] : FromAssumption p ioP P (le_upd_if b Q) where
-  from_assumption := h.1.trans le_upd_if_intro
-
 end If
 
 end Iris
diff --git a/Iris/Iris/Instances/Lib/NaInvariants.lean b/Iris/Iris/Instances/Lib/NaInvariants.lean
index afb706555..8df97d670 100644
--- a/Iris/Iris/Instances/Lib/NaInvariants.lean
+++ b/Iris/Iris/Instances/Lib/NaInvariants.lean
@@ -26,6 +26,9 @@ abbrev NaInvF : OFunctorPre :=
 class NaInvG (GF : BundledGFunctors) where
   inv : ElemG GF NaInvF
 
+#rocq_ignore «na_invΣ» "Superseded by the `NaInvG` typeclass on `BundledGFunctors`."
+#rocq_ignore «subG_na_invG» "Superseded by Lean's direct `ElemG` typeclass synthesis."
+
 attribute [reducible, instance] NaInvG.inv
 
 @[rocq_alias na_inv_pool_name]
diff --git a/Iris/Iris/Instances/Lib/Token.lean b/Iris/Iris/Instances/Lib/Token.lean
index 15d0729f2..626b6b8ae 100644
--- a/Iris/Iris/Instances/Lib/Token.lean
+++ b/Iris/Iris/Instances/Lib/Token.lean
@@ -26,17 +26,21 @@ FIXME: missing token_combine_gives
 abbrev TokenF : COFE.OFunctorPre := constOF (Excl Unit)
 
 @[rocq_alias tokenG]
-class TokenG (GF : BundledGFunctors) where
-  [elemG : ElemG GF TokenF]
+class TokenG (GF : BundledGFunctors) where [elemG : ElemG GF TokenF]
 
-attribute [reducible] TokenG.elemG
-attribute [instance] TokenG.elemG
+attribute [reducible, instance] TokenG.elemG
+
+#rocq_ignore «subG_tokenΣ» "Superseded by Lean's direct `ElemG` typeclass synthesis."
 
 variable {GF : BundledGFunctors} [TokenG GF]
 
 @[rocq_alias token]
 def token (γ : GName) : IProp GF := iOwn (F := TokenF) γ (excl ())
 
+#rocq_ignore token_aux "`token` is defined directly without `seal`/`unseal`."
+#rocq_ignore token_def "`token` is defined directly without `seal`/`unseal`."
+#rocq_ignore token_unseal "`token` is defined directly without `seal`/`unseal`."
+
 @[rocq_alias token_timeless]
 instance token_timeless (γ : GName) : Timeless (token (GF := GF) γ) := by
   unfold token
diff --git a/Iris/Iris/Instances/Lib/WSat.lean b/Iris/Iris/Instances/Lib/WSat.lean
index 78ae5ec9d..8b9d464b8 100644
--- a/Iris/Iris/Instances/Lib/WSat.lean
+++ b/Iris/Iris/Instances/Lib/WSat.lean
@@ -33,6 +33,7 @@ abbrev InvMap (x : Type _) := Std.ExtTreeMap Pos x compare
 abbrev InvMapF := HeapViewURF (F := PNat) (H := InvMap) (AgreeRF (LaterOF IdOF))
 
 /-- Wsat inclusion typeclass (`GF` contains the necessary functors for wsat) -/
+@[rocq_alias wsatGS.wsatGpreS]
 class WsatGpreS (GF : BundledGFunctors) where
   inv : ElemG GF InvMapF
   enabled : ElemG GF (constOF (DisjointLeibnizSet CoPset))
@@ -43,25 +44,33 @@ attribute [reducible, instance] WsatGpreS.enabled
 attribute [reducible, instance] WsatGpreS.disabled
 
 /-- Wsat allocated class (Names in a global IProp resource for the Wsat resources). -/
+@[rocq_alias wsatGS.wsatGS]
 class WsatGS (GF : BundledGFunctors) extends WsatGpreS GF where
   invariant_name : GName
   enabled_name : GName
   disabled_name : GName
 
+#rocq_ignore «wsatGS.wsatΣ» "Superseded by the `WsatGpreS` typeclass on `BundledGFunctors`."
+#rocq_ignore «wsatGS.subG_wsatΣ» "Superseded by Lean's direct `ElemG` typeclass synthesis."
+
 end WsatGS
 
 section Definitions
 
 variable {GF : BundledGFunctors} [W : WsatGS GF]
 
+@[rocq_alias invariant_unfold]
 abbrev invariant_unfold (P : IProp GF) : Later (IProp GF) := Later.next P
 
+@[rocq_alias ownI]
 def ownI (i : Pos) (P : IProp GF) : IProp GF :=
   iOwn (E := W.inv) W.invariant_name (Frag i discard (toAgree (invariant_unfold P)))
 
+@[rocq_alias ownE]
 def ownE (S : CoPset) : IProp GF :=
   iOwn (E := W.enabled) W.enabled_name (valid S)
 
+@[rocq_alias ownD]
 def ownD (S : PosSet) : IProp GF :=
   iOwn (E := W.disabled) W.disabled_name (valid S)
 
@@ -70,11 +79,15 @@ abbrev liftInv (I : InvMap (IProp GF)) := map toAgree (map invariant_unfold I)
 abbrev invMap (I : InvMap (IProp GF)) : InvMapF.ap (IProp GF) :=
   Auth (own 1) (liftInv I)
 
+@[rocq_alias wsat]
 def wsat : IProp GF := iprop(
   ∃ I : InvMap (IProp GF),
     iOwn (E := W.inv) W.invariant_name (invMap I) ∗
     [∗map] i ↦ Q ∈ I, (▷ Q ∗ ownD {i}) ∨ ownE {i})
 
+#rocq_ignore invariant_unfold_contractive "Only needed for ownI_contractive which is proved directly"
+
+@[rocq_alias ownI_contractive]
 instance (i : Pos) : Contractive (ownI (W := W) i) where
   distLater_dist h := by
     unfold ownI
@@ -83,6 +96,7 @@ instance (i : Pos) : Contractive (ownI (W := W) i) where
     refine NonExpansive.ne ?_
     exact Contractive.distLater_dist h
 
+@[rocq_alias ownI_persistent]
 instance (i : Pos) (P : IProp GF) : Persistent (ownI (W := W) i P) := by
   unfold ownI; infer_instance
 
@@ -92,13 +106,16 @@ section ownE
 
 variable {GF : BundledGFunctors} [W : WsatGS GF]
 
+@[rocq_alias ownE_empty]
 theorem ownE_empty : ⊢ |==> ownE (W := W) ∅ := iOwn_unit (ε := UCMRA.unit)
 
+@[rocq_alias ownE_op]
 theorem ownE_op {E1 E2} (Hdisj : E1 ## E2) : ownE (E1 ∪ E2) ⊣⊢@{IProp GF} ownE E1 ∗ ownE E2 := by
   refine .trans (.of_eq ?_) iOwn_op
   rw [disj_op_union Hdisj]
   rfl
 
+@[rocq_alias ownE_disjoint]
 theorem ownE_disjoint {E1 E2} : ownE E1 ∗ ownE E2 ⊢@{IProp GF} ⌜E1 ## E2⌝ := by
   iintro ⟨H1, H2⟩
   icases iOwn_op $$ [H1 H2] with H
@@ -109,6 +126,7 @@ theorem ownE_disjoint {E1 E2} : ownE E1 ∗ ownE E2 ⊢@{IProp GF} ⌜E1 ## E2
   ipure_intro
   exact valid_op_iff_disj.mp H
 
+@[rocq_alias ownE_op']
 theorem ownE_op_iff {E1 E2} : ⌜E1 ## E2⌝ ∧ ownE (E1 ∪ E2) ⊣⊢@{IProp GF} ownE E1 ∗ ownE E2 := by
   constructor
   · iintro ⟨%Hdisj, H⟩
@@ -122,7 +140,8 @@ theorem ownE_op_iff {E1 E2} : ⌜E1 ## E2⌝ ∧ ownE (E1 ∪ E2) ⊣⊢@{IProp
     · iapply (ownE_op Hdisj).mpr $$ [H1 H2]
       isplitl [H1] <;> iassumption
 
-theorem ownE_singleton_singleton {i : Pos} : ownE {i} ∗ ownE {i} ⊢@{IProp GF} False :=
+@[rocq_alias ownE_singleton_twice]
+theorem ownE_singleton_twice {i : Pos} : ownE {i} ∗ ownE {i} ⊢@{IProp GF} False :=
   ownE_disjoint.trans (pure_mono fun h => h i (by simp [mem_singleton]))
 
 end ownE
@@ -131,13 +150,16 @@ section ownD
 
 variable {GF : BundledGFunctors} [W : WsatGS GF]
 
+@[rocq_alias ownD_empty]
 theorem ownD_empty : ⊢@{IProp GF} |==> ownD ∅ := iOwn_unit (ε := UCMRA.unit)
 
+@[rocq_alias ownD_op]
 theorem ownD_op {E1 E2} (Hdisj : E1 ## E2) : ownD (E1 ∪ E2) ⊣⊢@{IProp GF} ownD E1 ∗ ownD E2 := by
   refine .trans (.of_eq ?_) iOwn_op
   rw [disj_op_union Hdisj]
   rfl
 
+@[rocq_alias ownD_disjoint]
 theorem ownD_disjoint (E1 E2 : PosSet) :
     ownD E1 ∗ ownD E2 ⊢@{IProp GF}  ⌜E1 ## E2⌝ := by
   unfold ownD
@@ -149,6 +171,7 @@ theorem ownD_disjoint (E1 E2 : PosSet) :
   ipure_intro
   exact valid_op_iff_disj.mp H
 
+@[rocq_alias ownD_op']
 theorem ownD_op_iff {E1 E2} : ⌜E1 ## E2⌝ ∧ ownD (E1 ∪ E2) ⊣⊢@{IProp GF} ownD E1 ∗ ownD E2 := by
   constructor
   · iintro ⟨%Hdisj, H⟩
@@ -162,6 +185,7 @@ theorem ownD_op_iff {E1 E2} : ⌜E1 ## E2⌝ ∧ ownD (E1 ∪ E2) ⊣⊢@{IProp
     · iapply (ownD_op Hdisj).mpr $$ [H1 H2]
       isplitl [H1] <;> iassumption
 
+@[rocq_alias ownD_singleton_twice]
 theorem ownD_singleton_twice {i : Pos} : ownD {i} ∗ ownD {i} ⊢@{IProp GF} False :=
     (ownD_disjoint {i} {i}).trans (pure_mono fun h => h i (by simp))
 
@@ -171,6 +195,7 @@ section operations
 
 variable {GF : BundledGFunctors} [W : WsatGS GF]
 
+@[rocq_alias invariant_lookup]
 theorem invariant_lookup (I : InvMap (IProp GF)) (i : Pos) (P : IProp GF) :
     iOwn (E := W.inv) W.invariant_name (invMap I) ∗ ownI i P
     ⊢@{IProp GF} ∃ Q, ⌜get? I i = .some Q⌝ ∗ ▷ internalEq Q P := by
@@ -190,6 +215,7 @@ theorem invariant_lookup (I : InvMap (IProp GF)) (i : Pos) (P : IProp GF) :
     rw [←Hagree]
     iapply toAgree_includedI $$ H2
 
+@[rocq_alias ownI_open]
 theorem ownI_open {i : Pos} {P : IProp GF} : wsat ∗ ownI i P ∗ ownE {i} ⊢ wsat ∗ ▷ P ∗ ownD {i} := by
   unfold wsat
   iintro ⟨⟨%I, Hown, Hmap⟩, #HI, HE⟩
@@ -209,9 +235,10 @@ theorem ownI_open {i : Pos} {P : IProp GF} : wsat ∗ ownI i P ∗ ownE {i} ⊢
         iapply internalEq.rewrite (Ψ := fun x => x) (hΨ := OFE.id_ne) $$ H HProp
       · iassumption
   · iexfalso
-    iapply ownE_singleton_singleton $$ [HE HE']
+    iapply ownE_singleton_twice $$ [HE HE']
     isplitl [HE] <;> iassumption
 
+@[rocq_alias ownI_close]
 theorem ownI_close {i : Pos} {P : IProp GF} : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {i} ⊢ wsat ∗ ownE {i} := by
   unfold wsat
   iintro ⟨⟨%I, Hown, Hmap⟩, #HI, HProp, HE⟩
@@ -239,6 +266,7 @@ section allocation
 
 variable {GF : BundledGFunctors}
 
+@[rocq_alias ownI_alloc]
 theorem ownI_alloc [W : WsatGS GF] (φ : Pos → Prop) (P : IProp GF)
     (Hfresh : ∀ E : PosSet, ∃ i, i ∉ E ∧ φ i) :
     ⊢ wsat ∗ ▷ P ==∗ ∃ i, ⌜φ i⌝ ∗ wsat ∗ ownI i P := by
@@ -280,6 +308,7 @@ theorem ownI_alloc [W : WsatGS GF] (φ : Pos → Prop) (P : IProp GF)
       · iexact Hmap
   · iexact Hpt
 
+@[rocq_alias ownI_alloc_open]
 theorem ownI_alloc_open [W : WsatGS GF] (φ : Pos → Prop) (P : IProp GF)
   (Hfresh : ∀ E : PosSet, ∃ i, i ∉ E ∧ φ i) :
   ⊢ wsat ==∗ ∃ i, ⌜φ i⌝ ∗ (ownE {i} -∗ wsat) ∗ ownI i P ∗ ownD {i} := by
@@ -320,6 +349,7 @@ theorem ownI_alloc_open [W : WsatGS GF] (φ : Pos → Prop) (P : IProp GF)
       · iexact Hmap
   · unfold ownI; rw [HEQ]; isplit <;> iassumption
 
+@[rocq_alias wsat_alloc]
 theorem wsat_alloc [WP : WsatGpreS GF] :
     ⊢ |==> ∃ (W : WsatGS GF), wsat (W := W) ∗ ownE ⊤ := by
   imod (iOwn_alloc (E := WP.inv) (Auth (.own 1) empty) auth_one_valid) with ⟨%γ, H⟩
diff --git a/Iris/Iris/Instances/UPred/Instance.lean b/Iris/Iris/Instances/UPred/Instance.lean
index 94956e511..9177fa4e7 100644
--- a/Iris/Iris/Instances/UPred/Instance.lean
+++ b/Iris/Iris/Instances/UPred/Instance.lean
@@ -25,22 +25,39 @@ variable [UCMRA M]
 
 section bidefs
 
+@[rocq_alias uPred_entails]
 protected def Entails (P Q : UPred M) : Prop := ∀ n (x : ValidAt M n), P n x → Q n x
 
+@[rocq_alias uPred_pure]
 protected def pure (p : Prop) : UPred M where
   holds _ _ := p
   mono h _ _ := h
 
+#rocq_ignore uPred.uPred_pure_unseal "`UPred.pure` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_si_pure_unseal "`UPred.uPredSiPure` is unsealed in Lean."
+#rocq_ignore uPred.uPred_si_emp_valid_unseal "`UPred.uPredSiEmpValid` is unsealed in Lean."
+
+@[rocq_alias uPred_and]
 protected def and (P Q : UPred M) : UPred M where
   holds n x := P n x ∧ Q n x
   mono HPQ Hle Hn := ⟨P.mono HPQ.1 Hle Hn, Q.mono HPQ.2 Hle Hn⟩
 
+#rocq_ignore uPred_and_unseal "`UPred.and` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_and_def "`UPred.and` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_and_aux "`UPred.and` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias uPred_or]
 protected def or (P Q : UPred M) : UPred M where
   holds n x := P n x ∨ Q n x
   mono
   | .inl H, Hle, Hn => .inl (P.mono H Hle Hn)
   | .inr H, Hle, Hn => .inr (Q.mono H Hle Hn)
 
+#rocq_ignore uPred_or_unseal "`UPred.or` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_or_def "`UPred.or` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_or_aux "`UPred.or` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias uPred_impl]
 protected def imp (P Q : UPred M) : UPred M where
   holds n x := ∀ {n'} (x' : ValidAt M n'), x.val ≼ x'.val → n' ≤ n → P n' x' → Q n' x'
   mono {_ _ x₁ x₂} H := fun ⟨m₁, Hle⟩ Hn n ⟨x, xP⟩ ⟨m₂, Hxle⟩ Hnle HP => by
@@ -54,18 +71,33 @@ protected def imp (P Q : UPred M) : UPred M where
     · exact Nat.le_trans Hnle Hn
     · exact (uPred_ne Hx).mp HP
 
+#rocq_ignore uPred_impl_unseal "`UPred.imp` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_impl_def "`UPred.imp` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_impl_aux "`UPred.imp` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias uPred_forall]
 protected def sForall (Ψ : UPred M → Prop) : UPred M where
   holds n x := ∀ p, Ψ p → p n x
   mono a a_1 a_2 p a_3 := p.mono (a p a_3) a_1 a_2
 
+#rocq_ignore uPred_forall_unseal "`UPred.sForall` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_forall_def "`UPred.sForall` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_forall_aux "`UPred.sForall` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias uPred_exist]
 protected def sExists (Ψ : UPred M → Prop) : UPred M where
   holds n x := ∃ p, Ψ p ∧ p n x
   mono := fun ⟨p, HΨ, Hp⟩ Hv Hn => ⟨p, HΨ, p.mono Hp Hv Hn⟩
 
+#rocq_ignore uPred_exist_unseal "`UPred.sExists` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_exist_def "`UPred.sExists` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_exist_aux "`UPred.sExists` is defined directly without `seal`/`unseal`."
+
 protected def eq [OFE O] (o1 o2 : O) : UPred M where
   holds n _ := o1 ≡{n}≡ o2
   mono H1 _ H2 := H1.le H2
 
+@[rocq_alias uPred_sep]
 protected def sep (P Q : UPred M) : UPred M where
   holds n x := ∃ x1 x2, ∃ (H : x.val ≡{n}≡ x1 • x2),
     P n ⟨x1, validN_op_left (validN_ne H x.property)⟩
@@ -78,6 +110,11 @@ protected def sep (P Q : UPred M) : UPred M where
     · exact P.mono HP (incN_refl x₁) Hn
     · exact Q.mono HQ (incN_op_left n₂ x₂ m) Hn
 
+#rocq_ignore uPred_sep_unseal "`UPred.sep` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_sep_aux "`UPred.sep` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_sep_def "`UPred.sep` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias uPred_wand]
 protected def wand (P Q : UPred M) : UPred M where
   holds n x := ∀ n' x', n' ≤ n → (H : ✓{n'} (x.val • x'))
     → P n' ⟨x', validN_op_right H⟩ → Q n' ⟨x • x', H⟩
@@ -86,20 +123,35 @@ protected def wand (P Q : UPred M) : UPred M where
       (op_monoN_left _ (incN_of_incN_le Hn' Hm)) .refl
     exact H _ _ (Nat.le_trans Hn' Hn) ?_ HP
 
+#rocq_ignore uPred_wand_unseal "`UPred.wand` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_wand_aux "`UPred.wand` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_wand_def "`UPred.wand` is defined directly without `seal`/`unseal`."
+
 protected def plainly (P : UPred M) : UPred M where
   holds n _ := P n ⟨unit, unit_validN⟩
   mono H _ Hn := P.mono H (incN_refl unit) Hn
 
+@[rocq_alias uPred_persistently]
 protected def persistently (P : UPred M) : UPred M where
   holds n x := P n ⟨core x, validN_core x.property⟩
   mono H Hx Hn := P.mono H (core_incN_core Hx) Hn
 
+#rocq_ignore uPred_persistently_unseal "`UPred.persistently` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_persistently_def "`UPred.persistently` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_persistently_aux "`UPred.persistently` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias uPred_later]
 protected def later (P : UPred M) : UPred M where
   holds n x := match n with | 0 => True | Nat.succ n' => P n' (x.le (Nat.le_succ _))
   mono {n₁ n₂} := by
     cases n₁ <;> cases n₂ <;> simp
     exact fun H Hx Hn => P.mono H (incN_of_incN_succ Hx) Hn
 
+#rocq_ignore uPred_later_unseal "`UPred.later` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_later_def "`UPred.later` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_later_aux "`UPred.later` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias uPred_ownM]
 def ownM (m : M) : UPred M where
   holds n x := m ≼{n} x
   mono {_ n₂ x₁ x₂} := fun ⟨m₁, Hm₁⟩ ⟨m₂, Hm₂⟩ Hn => by
@@ -108,10 +160,15 @@ def ownM (m : M) : UPred M where
          _      ≡{n₂}≡ (m • m₁) • m₂ := (Hm₁.le Hn).op_l
          _      ≡{n₂}≡ m • (m₁ • m₂) := assoc.symm.dist
 
+#rocq_ignore uPred_ownM_unseal "`UPred.ownM` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_ownM_def "`UPred.ownM` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_ownM_aux "`UPred.ownM` is defined directly without `seal`/`unseal`."
+
 def cmraValid {A} [CMRA A] (a : A) : UPred M where
   holds n _ := ✓{n} a
   mono hv _ le := validN_of_le le hv
 
+@[rocq_alias uPred_bupd]
 def bupd (Q : UPred M) : UPred M where
   holds n x := ∀ k yf, k ≤ n → ✓{k} (x.val • yf)
     → ∃ x', ∃ H : ✓{k} (x' • yf), Q k ⟨x', validN_op_left H⟩
@@ -127,6 +184,11 @@ def bupd (Q : UPred M) : UPred M where
     refine Q.mono HQ' ?_ k.le_refl
     exact incN_op_left k x' x3
 
+#rocq_ignore uPred_bupd_unseal "`UPred.bupd` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_bupd_def "`UPred.bupd` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_bupd_aux "`UPred.bupd` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias uPred_emp]
 protected def emp : UPred M where
   holds _ _ := True
   mono _ _ _ := trivial
@@ -148,7 +210,7 @@ instance later_contractive : OFE.Contractive UPred.later (α := UPred M) where
       | 0 => by simp [UPred.later]
       | n' + 1 => fun _ Hn' Hx' => Hl _ Hn' _ _ .refl (validN_succ Hx')
 
-@[rocq_alias uPred_primitive.ownM_ne]
+@[rocq_alias uPred_primitive.ownM_ne, rocq_alias uPred.ownM_ne]
 instance ownM_ne : OFE.NonExpansive (ownM : M → UPred M) where
   ne _ _ _ H _ _ Hn _ := OFE.Dist.incN (OFE.Dist.le H Hn) .rfl
 
@@ -184,10 +246,31 @@ instance : BIBase (UPred M) where
   persistently := UPred.persistently
   later        := UPred.later
 
+
+#rocq_ignore uPred.uPred_emp_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_pure_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_si_pure_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_si_emp_valid_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_and_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_or_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_impl_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_forall_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_exist_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_sep_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_wand_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_persistently_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_later_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_bupd_unseal "Connectives are defined directly without `seal`/`unseal`."
+#rocq_ignore uPred.uPred_unseal "No `Ltac unseal` rewrite is needed; nothing is sealed."
+
+#rocq_ignore uPred_primitive.uPred_unseal "No `Ltac unseal` rewrite is needed; nothing is sealed."
+
+@[rocq_alias uPred_primitive.entails_po]
 instance uPred_entails_preorder : Std.Preorder (Entails (PROP := UPred M)) where
   refl _ _ H := H
   trans H1 H2 _ _ Hv := H2 _ _ <| H1 _ _ Hv
 
+@[rocq_alias uPred_primitive.entails_lim]
 theorem uPred_entails_lim {cP cQ : Chain (UPred M)} (H : ∀ n, cP n ⊢ cQ n) :
     IsCOFE.compl cP ⊢ IsCOFE.compl cQ := by
   intros n Hv HP
@@ -195,6 +278,7 @@ theorem uPred_entails_lim {cP cQ : Chain (UPred M)} (H : ∀ n, cP n ⊢ cQ n) :
   refine H _ _ Hv ?_
   exact uPred_holds_ne IsCOFE.conv_compl.symm n.le_refl _ Hv.property HP
 
+@[rocq_alias uPredI]
 instance : BI (UPred M) where
   entails_preorder := inferInstance
   equiv_iff {_ _} := by
@@ -340,10 +424,70 @@ instance : BI (UPred M) where
     | 0, _, _ => .inl trivial
     | _+1, _, H => .inr @fun | 0, _, Hx'le, _, _ => P.mono H Hx'le.incN (Nat.zero_le _)
 
+
+#rocq_ignore pure_intro "Inlined in `uPredI` construction"
+#rocq_ignore pure_elim' "Inlined in `uPredI` construction"
+
+#rocq_ignore uPred_primitive.and_elim_l "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.and_elim_r "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.and_intro "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.and_ne "Inlined in `uPredI` construction"
+
+#rocq_ignore uPred_primitive.or_intro_l "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.or_intro_r "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.or_elim "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.or_ne "Inlined in `uPredI` construction"
+
+#rocq_ignore uPred_primitive.impl_elim_l' "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.impl_intro_r "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.impl_ne "Inlined in `uPredI` construction"
+
+#rocq_ignore uPred_primitive.sep_assoc' "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.sep_comm' "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.sep_mono "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.sep_ne "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.True_sep_1 "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.True_sep_2 "Inlined in `uPredI` construction"
+
+#rocq_ignore uPred_primitive.wand_elim_l' "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.wand_intro_r "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.wand_ne "Inlined in `uPredI` construction"
+
+#rocq_ignore uPred_primitive.persistently_and_sep_l_1 "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.persistently_exist_1 "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.persistently_idemp_2 "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.persistently_mono "Inlined in `uPredI` construction"
+
+#rocq_ignore uPred_primitive.exist_elim "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.exist_intro "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.exist_ne "Inlined in `uPredI` construction"
+
+#rocq_ignore uPred_primitive.forall_elim "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.forall_intro "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.forall_ne "Inlined in `uPredI` construction"
+
+#rocq_ignore uPred_primitive.later_intro "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.later_mono "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.later_sep_1 "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.later_sep_2 "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.later_persistently_1 "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.later_persistently_2 "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.later_exist_false "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.later_false_em "Inlined in `uPredI` construction"
+#rocq_ignore uPred_primitive.later_forall_2 "Inlined in `uPredI` construction"
+
+#rocq_ignore uPred_bi_mixin "Inlined in `uPredI` construction"
+#rocq_ignore uPred_bi_later_mixin "Inlined in `uPredI` construction"
+#rocq_ignore uPred_bi_persistently_mixin "Inlined in `uPredI` construction"
+
 @[rocq_alias uPred_persistently_forall]
 instance : BIPersistentlyForall (UPred M) where
   persistently_sForall_2 _ _ x h p hp := h _ ⟨p, rfl⟩ x (inc_refl _) .refl hp
 
+#rocq_ignore uPred_primitive.persistently_forall_2 "Inlined in `BIPersistentlyForall` construction"
+
+#rocq_ignore uPred_pure_forall "BiPureForall is not needed"
+
 @[rocq_alias uPred_later_contractive]
 instance : BILaterContractive (UPred M) where
   toContractive := later_contractive
@@ -354,19 +498,29 @@ instance (P : UPred M) : Affine P where
 @[rocq_alias uPred_affine]
 instance : BIAffine (UPred M) := ⟨by infer_instance⟩
 
+@[rocq_alias uPred_si_pure]
 protected def uPredSiPure (Pi : SiProp) : UPred M where
   holds n _ := Pi.holds n
   mono H _ Hn := Pi.closed H Hn
 
+#rocq_ignore uPred_si_pure_aux "`UPred.uPredSiPure` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_si_pure_unseal "`UPred.uPredSiPure` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_si_pure_def "`UPred.uPredSiPure` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias uPred_si_emp_valid]
 protected def uPredSiEmpValid (P : UPred M) : SiProp where
   holds n := P n ⟨unit, unit_validN⟩
   closed h hle := P.mono h (incN_refl _) hle
 
-@[rocq_alias si_pure_ne]
+#rocq_ignore uPred_si_emp_valid_aux "`UPred.uPredSiEmpValid` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_si_emp_valid_unseal "`UPred.uPredSiEmpValid` is defined directly without `seal`/`unseal`."
+#rocq_ignore uPred_si_emp_valid_def "`UPred.uPredSiEmpValid` is defined directly without `seal`/`unseal`."
+
+@[rocq_alias si_pure_ne, rocq_alias uPred_primitive.si_pure_ne]
 instance uPredSiPure_ne : OFE.NonExpansive (UPred.uPredSiPure : SiProp → UPred M) where
   ne _ _ _ hp _ _ hn _ := hp hn
 
-@[rocq_alias si_emp_valid_ne]
+@[rocq_alias si_emp_valid_ne, rocq_alias uPred_primitive.si_emp_valid_ne]
 instance uPredSiEmpValid_ne : OFE.NonExpansive (UPred.uPredSiEmpValid : UPred M → SiProp) where
   ne _ _ _ h m hm := h m unit hm unit_validN
 
@@ -380,55 +534,43 @@ section SiPropEmbedding
 ## Rules for the SiProp embedding
 -/
 
-@[rocq_alias si_pure_mono]
+@[rocq_alias si_pure_mono, rocq_alias uPred_primitive.si_pure_mono]
 theorem uPredSiPure_mono {Pi Qi : SiProp} (hpq : Pi ⊢ Qi) : <si_pure> Pi ⊢@{UPred M} <si_pure> Qi :=
   fun n _ hp => hpq n hp
 
-@[rocq_alias si_emp_valid_mono]
+@[rocq_alias si_emp_valid_mono, rocq_alias uPred_primitive.si_emp_valid_mono]
 theorem uPredSiEmpValid_mono {P Q : UPred M} (h : P ⊢ Q) : <si_emp_valid> P ⊢ <si_emp_valid> Q :=
   fun n hp => h n ⟨unit, unit_validN⟩ hp
 
-@[rocq_alias si_pure_impl_2]
+@[rocq_alias si_pure_impl_2, rocq_alias uPred_primitive.si_pure_impl_2]
 theorem uPredSiPure_imp_mpr {Pi Qi : SiProp} :
     (<si_pure> Pi → <si_pure> Qi) ⊢@{UPred M} <si_pure> (Pi → Qi) :=
   fun _ x hpq _ hle => hpq (x.le hle) .rfl hle
 
-@[rocq_alias si_pure_later]
+@[rocq_alias si_pure_later, rocq_alias uPred_primitive.si_pure_later]
 theorem uPredSiPure_later {Pi : SiProp} : <si_pure> (▷ Pi) ⊣⊢@{UPred M} ▷ <si_pure> Pi :=
   ⟨fun | 0, _ | _+1, _ => id, fun | 0, _ | _+1, _ => id⟩
 
-@[rocq_alias si_emp_valid_later_1]
+@[rocq_alias si_emp_valid_later_1, rocq_alias uPred_primitive.si_emp_valid_later_1]
 theorem uPredSiEmpValid_later_mp {P : UPred M} : <si_emp_valid> (▷ P) ⊢ ▷ <si_emp_valid> P :=
   fun | 0 | _+1 => id
 
-@[rocq_alias si_emp_valid_si_pure]
+@[rocq_alias si_emp_valid_si_pure, rocq_alias uPred_primitive.si_emp_valid_si_pure]
 theorem uPredSiEmpValid_uPredSiPure {Pi : SiProp} : <si_emp_valid> (<si_pure> Pi : UPred M) ⊣⊢ Pi :=
   ⟨fun _ hp => hp, fun _ hp => hp⟩
 
-@[rocq_alias si_pure_si_emp_valid]
+@[rocq_alias si_pure_si_emp_valid, rocq_alias uPred_primitive.si_pure_si_emp_valid]
 theorem uPredSiPure_uPredSiEmpValid {P : UPred M} : <si_pure> <si_emp_valid> P ⊢ <pers> P :=
   fun n _ hp => P.mono hp incN_unit n.le_refl
 
-@[rocq_alias persistently_impl_si_pure]
+@[rocq_alias persistently_impl_si_pure, rocq_alias uPred_primitive.persistently_impl_si_pure]
 theorem persistently_imp_uPredSiPure {Pi : SiProp} {Q : UPred M} :
     (<si_pure> Pi → <pers> Q) ⊢ <pers> (<si_pure> Pi → Q) := by
   intro n x hpq m y hinc hle hp
   have hq := hpq (x.le hle) (inc_refl x.val) hle hp
   exact Q.mono hq hinc.incN m.le_refl
 
--- si_pure_forall_2 is already in Sbi.lean
-theorem uPredSiPure_forall_mpr {α : Type _} {Pi : α → SiProp} :
-    (∀ x, <si_pure> Pi x : UPred M) ⊢ <si_pure> (∀ x, Pi x) := by
-  rintro _ _ hp _ ⟨a, rfl⟩
-  exact hp iprop(<si_pure> Pi a) ⟨a, rfl⟩
-
--- si_emp_valid_exist_1 is already in Sbi.lean
-theorem uPredSiEmpValid_exist_mp {α : Type _} {P : α → UPred M} :
-    (<si_emp_valid> (∃ x, P x) : SiProp) ⊢ ∃ x, <si_emp_valid> P x := by
-  rintro _ ⟨_, ⟨a, rfl⟩, hp⟩
-  exact ⟨iprop(<si_emp_valid> P a), ⟨a, rfl⟩, hp⟩
-
--- prop_ext_2 is already in SIProp.lean
+@[rocq_alias uPred_primitive.prop_ext_2]
 theorem prop_ext_uPredSiEmpValid {P Q : UPred M} : <si_emp_valid> (P ∗-∗ Q) ⊢ SiProp.internalEq P Q := by
   intro _ hpq n x hn hv
   have hu : unit • x ≡{n}≡ x := unit_left_id.dist
@@ -439,6 +581,7 @@ theorem prop_ext_uPredSiEmpValid {P Q : UPred M} : <si_emp_valid> (P ∗-∗ Q)
 
 end SiPropEmbedding
 
+@[rocq_alias uPred_sbi]
 instance : Sbi (UPred M) where
   siPure_ne := uPredSiPure_ne
   siEmpValid_ne := uPredSiEmpValid_ne
@@ -455,12 +598,23 @@ instance : Sbi (UPred M) where
   siEmpValid_affinely_mpr _ h := ⟨trivial, h⟩
   prop_ext_siEmpValid := prop_ext_uPredSiEmpValid
 
+#rocq_ignore uPred_sbi_mixin "Inlined in uPred_sbi construction"
+#rocq_ignore uPred_sbi_prop_ext_mixin "Inlined in uPred_sbi construction"
+
+@[rocq_alias uPred_primitive.si_pure_forall_2]
+theorem uPredSiPure_forall_mpr {α : Type _} {Pi : α → SiProp} :
+    (∀ x, <si_pure> Pi x : UPred M) ⊢ <si_pure> (∀ x, Pi x) := siPure_forall_mpr
+
 @[rocq_alias uPred_sbi_emp_valid_exist]
 instance : SbiEmpValidExist (UPred M) where
   siEmpValid_sExists_1 Ψ n h := by
     obtain ⟨p, hΨ, hp⟩ := h
     exact ⟨_, ⟨p, rfl⟩, hΨ, hp⟩
 
+@[rocq_alias uPred_primitive.si_emp_valid_exist_1]
+theorem uPredSiEmpValid_exist_mp {α : Type _} {P : α → UPred M} :
+    (<si_emp_valid> (∃ x, P x) : SiProp) ⊢ ∃ x, <si_emp_valid> P x := siEmpValid_exist_mp
+
 /-- The Sbi-derived plainly on UPred unfolds to `UPred.plainly`. -/
 theorem plainly_eq_uPred_plainly (P : UPred M) : iprop(■ P) = UPred.plainly P := rfl
 
@@ -487,6 +641,12 @@ instance : BIUpdate (UPred M) where
     refine ⟨x' • x2, op_assocN.validN.1 Hx'1, x', x2, .rfl, Hx'2, ?_⟩
     exact R.mono HR (incN_refl x2) Hk
 
+#rocq_ignore uPred_primitive.bupd_intro "Inlined in BIUpdate instance construction"
+#rocq_ignore uPred_primitive.bupd_mono "Inlined in BIUpdate instance construction"
+#rocq_ignore uPred_primitive.bupd_trans "Inlined in BIUpdate instance construction"
+#rocq_ignore uPred_primitive.bupd_frame_r "Inlined in BIUpdate instance construction"
+#rocq_ignore uPred_bupd_mixin "Inlined in BIUpdate instance construction"
+
 @[rocq_alias uPred_primitive.bupd_si_pure]
 theorem bupd_si_pure (Pi : SiProp) : (|==> <si_pure> Pi : UPred M) ⊢ <si_pure> Pi := by
   intro n x Hv
@@ -505,10 +665,10 @@ instance : BIBUpdatePlainly (UPred M) where
     rw [plainly_eq_uPred_plainly] at Hx'
     exact P.mono Hx' incN_unit n.le_refl
 
-@[rocq_alias uPred_primitive.ownM_valid]
+@[rocq_alias uPred_primitive.ownM_valid, rocq_alias uPred.ownM_valid]
 theorem ownM_valid (m : M) : ownM m ⊢ internalCmraValid m := fun _ h hp => hp.validN h.property
 
-@[rocq_alias uPred_primitive.ownM_op]
+@[rocq_alias uPred_primitive.ownM_op, rocq_alias uPred.ownM_op]
 theorem ownM_op (m1 m2 : M) : ownM (m1 • m2) ⊣⊢ ownM m1 ∗ ownM m2 := by
   constructor
   · intro n _ ⟨z, Hz⟩
@@ -531,11 +691,11 @@ theorem ownM_eqv {m1 m2 : M} (H : m1 ≡ m2) : ownM m1 ⊣⊢ ownM m2 :=
 theorem ownM_always_invalid_elim (m : M) (H : ∀ n, ¬✓{n} m) : internalCmraValid m ⊢@{UPred M} False :=
   fun n _ => H n
 
-@[rocq_alias uPred.ownM_unit]
+@[rocq_alias uPred.ownM_unit, rocq_alias uPred_primitive.ownM_unit]
 theorem ownM_unit P : P ⊢ □ ownM (unit : M) :=
   fun _ _ _ => ⟨trivial, incN_unit⟩
 
-@[rocq_alias uPred.persistently_ownM_core]
+@[rocq_alias uPred.persistently_ownM_core, rocq_alias uPred_primitive.persistently_ownM_core]
 theorem persistently_ownM_core (a : M) : ownM a ⊢ <pers> ownM (core a) :=
   fun _ _ => core_incN_core
 
@@ -550,7 +710,7 @@ instance {a : M} : Persistent (ownM (core a)) where
     refine OFE.NonExpansive.eqv ?_
     exact core_idem a
 
-@[rocq_alias uPred.bupd_ownM_updateP]
+@[rocq_alias uPred.bupd_ownM_updateP, rocq_alias uPred_primitive.bupd_ownM_updateP]
 theorem bupd_ownM_updateP (x : M) (Φ : M → Prop) :
   (x ~~>: Φ) → ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ ownM y := by
   intro Hup _ _ ⟨x3, Hx⟩ k yf Hk Hyf
@@ -563,7 +723,7 @@ theorem bupd_ownM_updateP (x : M) (Φ : M → Prop) :
   · exists y
   · exact ⟨HΦy, incN_op_left k y x3⟩
 
-@[rocq_alias uPred.ownM_forall]
+@[rocq_alias uPred.ownM_forall, rocq_alias uPred_primitive.ownM_forall]
 theorem ownM_forall (f : A → M) :
   (∀ a, ownM (f a)) ⊢ ∃ z, ownM z ∧ (∀ a, ∃ xf, UPred.eq z (f a • xf)) := by
   intro _ x Hf
@@ -573,7 +733,7 @@ theorem ownM_forall (f : A → M) :
   rcases Hf (ownM (f a)) ⟨a, rfl⟩ with ⟨xf, Hxf⟩
   exact ⟨(UPred.eq x.val (f a • xf)), ⟨xf, rfl⟩, Hxf⟩
 
-@[rocq_alias uPred.later_ownM]
+@[rocq_alias uPred.later_ownM, rocq_alias uPred_primitive.later_ownM]
 theorem later_ownM (a : M) : ▷ ownM a ⊢ ∃ b, ownM b ∧ ▷ <si_pure> (SiProp.internalEq a b)
   | 0, _, _ =>
     ⟨iprop(ownM unit ∧ ▷ <si_pure> (SiProp.internalEq a unit)), ⟨unit, rfl⟩, incN_unit, trivial⟩
diff --git a/Iris/Iris/Std/Namespaces.lean b/Iris/Iris/Std/Namespaces.lean
index 089591c4f..5eeb719a6 100644
--- a/Iris/Iris/Std/Namespaces.lean
+++ b/Iris/Iris/Std/Namespaces.lean
@@ -8,6 +8,7 @@ module
 public import Iris.Std.CoPset
 public import Iris.Std.Positives
 public import Iris.Std.GenSets
+meta import Iris.Std.RocqPorting
 
 @[expose] public section
 
@@ -68,6 +69,7 @@ theorem nclose_not_finite (N : Namespace) : ¬CoPset.isFinite (↑N) := by
   simp only [nclose]
   exact CoPset.suffixes_not_finite (Pos.flatten N)
 
+@[rocq_alias fresh_inv_name]
 theorem fresh_name {S : Type _} [Iris.Std.LawfulFiniteSet S Pos] (E : S) (N : Namespace) :
   ∃ i, i ∉ E ∧ i ∈ (↑N : CoPset) := by
   exists (CoPset.pick (↑N \ set_to_coPset E))
diff --git a/scripts/check_porting.py b/scripts/check_porting.py
index 9a1bdcdff..1819e50da 100755
--- a/scripts/check_porting.py
+++ b/scripts/check_porting.py
@@ -84,8 +84,10 @@ def log(msg: str) -> None:
 )
 
 # Module/Section tracking: Modules qualify names (e.g., Module bi -> bi.foo),
-# but Sections do not. 
-_MODULE_START_RE = re.compile(r"^\s*Module\s+(\w+)", re.MULTILINE)
+# but Sections do not.
+# `Module Export M` and `Module Import M` are valid forms where the name is M,
+# not the Export/Import keyword.
+_MODULE_START_RE = re.compile(r"^\s*Module\s+(?:Export\s+|Import\s+)?(\w+)", re.MULTILINE)
 _MODULE_TYPE_RE = re.compile(r"^\s*Module\s+Type\b")  # Module Types are skipped
 _SECTION_START_RE = re.compile(r"^\s*Section\s+(\w+)", re.MULTILINE)
 _END_RE = re.compile(r"^\s*End\s+(\w+)\s*\.", re.MULTILINE)