diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index c96fc87bda2ab76bf8934562d081921faeeb9fcb..6400459780ec5b8dff0a327426f694bbf4b62d2e 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -315,7 +315,8 @@ Qed.
 Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
   `{!Contractive f} : A := compl (fixpoint_chain f).
 Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
-Definition fixpoint {A AC AiH} f {Hf} := fixpoint_aux.(unseal) A AC AiH f Hf.
+Definition fixpoint := fixpoint_aux.(unseal).
+Arguments fixpoint {A _ _} f {_}.
 Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
 
 Section fixpoint.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 6cdf3d284cc2c909e4bbaa9110099bc4849cca24..a9867444208f8cdf3ea4028556aa3b01e5141183 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -9,10 +9,11 @@ Import uPred.
 
 Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P).
-Definition uPred_fupd_aux `{!invG Σ} : seal uPred_fupd_def. Proof. by eexists. Qed.
-Definition uPred_fupd `{!invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
-Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
-  uPred_fupd_aux.(seal_eq).
+Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
+Definition uPred_fupd := uPred_fupd_aux.(unseal).
+Arguments uPred_fupd {Σ _}.
+Lemma uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
+Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
 
 Lemma uPred_fupd_mixin `{!invG Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
 Proof.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 5eeff6cdb5bb9a37c39204d345d56c12c3b2f9e3..efe8eb9b2059770cfc69852d98f83ec8cbbb5756 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -75,8 +75,8 @@ Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
   gen_heap_name : gname;
   gen_meta_name : gname
 }.
-Arguments gen_heap_name {_ _ _ _ _} _ : assert.
-Arguments gen_meta_name {_ _ _ _ _} _ : assert.
+Arguments gen_heap_name {L V Σ _ _} _ : assert.
+Arguments gen_meta_name {L V Σ _ _} _ : assert.
 
 Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
   gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V));
@@ -121,9 +121,10 @@ Section definitions.
     ∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
           own γm (namespace_map_data N (to_agree (encode x))).
   Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
-  Definition meta {A dA cA} := meta_aux.(unseal) A dA cA.
+  Definition meta := meta_aux.(unseal).
   Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
 End definitions.
+Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
 Local Notation "l ↦{ q } v" := (mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 9362abc84e49e137ca3fe946a10cc5ae13799f31..4ddbe68958da21bc8cc39ce7f8fdd54b731cfcb6 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -10,10 +10,10 @@ Import uPred.
 Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   □ ∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True).
 Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
-Definition inv {Σ i} := inv_aux.(unseal) Σ i.
+Definition inv := inv_aux.(unseal).
+Arguments inv {Σ _} N P.
 Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
 Instance: Params (@inv) 3 := {}.
-Typeclasses Opaque inv.
 
 (** * Invariants *)
 Section inv.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index ce5889435a70183a6aecfddc058f941e8fe9e73e..ed77ef6f19e44e81add28bea10c5f2a00aff89a2 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -58,10 +58,10 @@ Instance: Params (@iRes_singleton) 4 := {}.
 Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
   uPred_ownM (iRes_singleton γ a).
 Definition own_aux : seal (@own_def). Proof. by eexists. Qed.
-Definition own {Σ A i} := own_aux.(unseal) Σ A i.
+Definition own := own_aux.(unseal).
+Arguments own {Σ A _} γ a.
 Definition own_eq : @own = @own_def := own_aux.(seal_eq).
 Instance: Params (@own) 4 := {}.
-Typeclasses Opaque own.
 
 (** * Properties about ghost ownership *)
 Section global.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index b84f1a1ddc7f150cd5089d74c8216009b5d882b0..fe44e03230e8ab0cde1d8fd13a986b0e558ae034 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -193,7 +193,8 @@ Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
   {| uPred_holds n x := φ |}.
 Solve Obligations with done.
 Definition uPred_pure_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
-Definition uPred_pure {M} := uPred_pure_aux.(unseal) M.
+Definition uPred_pure := uPred_pure_aux.(unseal).
+Arguments uPred_pure {M}.
 Definition uPred_pure_eq :
   @uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
 
@@ -201,14 +202,16 @@ Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := P n x ∧ Q n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_and_aux : seal (@uPred_and_def). Proof. by eexists. Qed.
-Definition uPred_and {M} := uPred_and_aux.(unseal) M.
+Definition uPred_and := uPred_and_aux.(unseal).
+Arguments uPred_and {M}.
 Definition uPred_and_eq: @uPred_and = @uPred_and_def := uPred_and_aux.(seal_eq).
 
 Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := P n x ∨ Q n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_or_aux : seal (@uPred_or_def). Proof. by eexists. Qed.
-Definition uPred_or {M} := uPred_or_aux.(unseal) M.
+Definition uPred_or := uPred_or_aux.(unseal).
+Arguments uPred_or {M}.
 Definition uPred_or_eq: @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).
 
 Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
@@ -220,7 +223,8 @@ Next Obligation.
   eapply HPQ; auto. exists (x2 â‹… x4); by rewrite assoc.
 Qed.
 Definition uPred_impl_aux : seal (@uPred_impl_def). Proof. by eexists. Qed.
-Definition uPred_impl {M} := uPred_impl_aux.(unseal) M.
+Definition uPred_impl := uPred_impl_aux.(unseal).
+Arguments uPred_impl {M}.
 Definition uPred_impl_eq :
   @uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
 
@@ -228,7 +232,8 @@ Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M :=
   {| uPred_holds n x := ∀ a, Ψ a n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_forall_aux : seal (@uPred_forall_def). Proof. by eexists. Qed.
-Definition uPred_forall {M A} := uPred_forall_aux.(unseal) M A.
+Definition uPred_forall := uPred_forall_aux.(unseal).
+Arguments uPred_forall {M A}.
 Definition uPred_forall_eq :
   @uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
 
@@ -236,14 +241,16 @@ Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M :=
   {| uPred_holds n x := ∃ a, Ψ a n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_exist_aux : seal (@uPred_exist_def). Proof. by eexists. Qed.
-Definition uPred_exist {M A} := uPred_exist_aux.(unseal) M A.
+Definition uPred_exist := uPred_exist_aux.(unseal).
+Arguments uPred_exist {M A}.
 Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).
 
 Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M :=
   {| uPred_holds n x := a1 ≡{n}≡ a2 |}.
 Solve Obligations with naive_solver eauto 2 using dist_le.
 Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). Proof. by eexists. Qed.
-Definition uPred_internal_eq {M A} := uPred_internal_eq_aux.(unseal) M A.
+Definition uPred_internal_eq := uPred_internal_eq_aux.(unseal).
+Arguments uPred_internal_eq {M A}.
 Definition uPred_internal_eq_eq:
   @uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
 
@@ -255,7 +262,8 @@ Next Obligation.
   eapply dist_le, Hn. by rewrite Hy Hx assoc.
 Qed.
 Definition uPred_sep_aux : seal (@uPred_sep_def). Proof. by eexists. Qed.
-Definition uPred_sep {M} := uPred_sep_aux.(unseal) M.
+Definition uPred_sep := uPred_sep_aux.(unseal).
+Arguments uPred_sep {M}.
 Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).
 
 Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
@@ -267,7 +275,8 @@ Next Obligation.
     eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
 Qed.
 Definition uPred_wand_aux : seal (@uPred_wand_def). Proof. by eexists. Qed.
-Definition uPred_wand {M} := uPred_wand_aux.(unseal) M.
+Definition uPred_wand := uPred_wand_aux.(unseal).
+Arguments uPred_wand {M}.
 Definition uPred_wand_eq :
   @uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).
 
@@ -278,7 +287,8 @@ Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n ε |}.
 Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
 Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. by eexists. Qed.
-Definition uPred_plainly {M} := uPred_plainly_aux.(unseal) M.
+Definition uPred_plainly := uPred_plainly_aux.(unseal).
+Arguments uPred_plainly {M}.
 Definition uPred_plainly_eq :
   @uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
 
@@ -286,7 +296,8 @@ Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
 Solve Obligations with naive_solver eauto using uPred_mono, cmra_core_monoN.
 Definition uPred_persistently_aux : seal (@uPred_persistently_def). Proof. by eexists. Qed.
-Definition uPred_persistently {M} := uPred_persistently_aux.(unseal) M.
+Definition uPred_persistently := uPred_persistently_aux.(unseal).
+Arguments uPred_persistently {M}.
 Definition uPred_persistently_eq :
   @uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).
 
@@ -296,7 +307,8 @@ Next Obligation.
   intros M P [|n1] [|n2] x1 x2; eauto using uPred_mono, cmra_includedN_S with lia.
 Qed.
 Definition uPred_later_aux : seal (@uPred_later_def). Proof. by eexists. Qed.
-Definition uPred_later {M} := uPred_later_aux.(unseal) M.
+Definition uPred_later := uPred_later_aux.(unseal).
+Arguments uPred_later {M}.
 Definition uPred_later_eq :
   @uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
 
@@ -307,7 +319,8 @@ Next Obligation.
   exists (a' â‹… x2). by rewrite Hx(assoc op) Hx1.
 Qed.
 Definition uPred_ownM_aux : seal (@uPred_ownM_def). Proof. by eexists. Qed.
-Definition uPred_ownM {M} := uPred_ownM_aux.(unseal) M.
+Definition uPred_ownM := uPred_ownM_aux.(unseal).
+Arguments uPred_ownM {M}.
 Definition uPred_ownM_eq :
   @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
 
@@ -315,7 +328,8 @@ Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M :=
   {| uPred_holds n x := ✓{n} a |}.
 Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
 Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). Proof. by eexists. Qed.
-Definition uPred_cmra_valid {M A} := uPred_cmra_valid_aux.(unseal) M A.
+Definition uPred_cmra_valid := uPred_cmra_valid_aux.(unseal).
+Arguments uPred_cmra_valid {M A}.
 Definition uPred_cmra_valid_eq :
   @uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
 
@@ -330,7 +344,8 @@ Next Obligation.
   eauto using uPred_mono, cmra_includedN_l.
 Qed.
 Definition uPred_bupd_aux : seal (@uPred_bupd_def). Proof. by eexists. Qed.
-Definition uPred_bupd {M} := uPred_bupd_aux.(unseal) M.
+Definition uPred_bupd := uPred_bupd_aux.(unseal).
+Arguments uPred_bupd {M}.
 Definition uPred_bupd_eq :
   @uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq).
 
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index fdf1fe18246d10ffbab0f0532579db9220d32e7f..768a357574099eea137bb9fb49594412fe1e93fa 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -57,7 +57,7 @@ Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
 Definition big_sepM2_aux : seal (@big_sepM2_def). Proof. by eexists. Qed.
 Definition big_sepM2 := big_sepM2_aux.(unseal).
 Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
-Definition big_sepM2_eq : @big_sepM2 = @big_sepM2_def := big_sepM2_aux.(seal_eq).
+Definition big_sepM2_eq : @big_sepM2 = _ := big_sepM2_aux.(seal_eq).
 Instance: Params (@big_sepM2) 6 := {}.
 Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
   (big_sepM2 (λ k x1 x2, P) m1 m2) : bi_scope.
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 3e695fcffc28592274fc2229206cacd1b6b92995..bea7c66396f0ac47a3191c5da84fc066bc647771 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -88,9 +88,9 @@ End definition.
 
 (** Seal it *)
 Definition atomic_update_aux : seal (@atomic_update_def). Proof. by eexists. Qed.
-Definition atomic_update `{BiFUpd PROP} {TA TB : tele} := atomic_update_aux.(unseal) PROP _ TA TB.
-Definition atomic_update_eq :
-  @atomic_update = @atomic_update_def := atomic_update_aux.(seal_eq).
+Definition atomic_update := atomic_update_aux.(unseal).
+Arguments atomic_update {PROP _ TA TB}.
+Definition atomic_update_eq : @atomic_update = _ := atomic_update_aux.(seal_eq).
 
 Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
 Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 6df3cd65d2583a77bddd51459d597b446ae4bc13..7202ef3753e612b404fbd8b9f495a2601a06cda5 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -1,5 +1,6 @@
 From stdpp Require Import coPset.
 From iris.bi Require Import bi.
+Set Default Proof Using "Type".
 
 (** Definitions. *)
 Structure biIndex :=
@@ -126,9 +127,9 @@ Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
   MonPred (λ i, (∀ j, ⌜i ⊑ j⌝ → Φ j)%I) _.
 Next Obligation. solve_proper. Qed.
 
-Definition monPred_embed_def (P : PROP) : monPred := MonPred (λ _, P) _.
+Definition monPred_embed_def : Embed PROP monPred := λ (P : PROP), MonPred (λ _, P) _.
 Definition monPred_embed_aux : seal (@monPred_embed_def). Proof. by eexists. Qed.
-Definition monPred_embed : Embed PROP monPred := monPred_embed_aux.(unseal).
+Definition monPred_embed := monPred_embed_aux.(unseal).
 Definition monPred_embed_eq : @embed _ _ monPred_embed = _ := monPred_embed_aux.(seal_eq).
 
 Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
@@ -743,10 +744,11 @@ Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply objectiv
 Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
   MonPred (λ i, |==> P i)%I _.
 Next Obligation. solve_proper. Qed.
-Definition monPred_bupd_aux `{BiBUpd PROP} : seal monPred_bupd_def. Proof. by eexists. Qed.
-Definition monPred_bupd `{BiBUpd PROP} : BUpd _ := monPred_bupd_aux.(unseal).
-Definition monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = _ :=
-  monPred_bupd_aux.(seal_eq).
+Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
+Definition monPred_bupd := monPred_bupd_aux.(unseal).
+Arguments monPred_bupd {_}.
+Lemma monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
+Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
 
 Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
 Proof.
@@ -807,11 +809,13 @@ Proof. rewrite /bi_except_0. apply _. Qed.
 (** Internal equality *)
 Definition monPred_internal_eq_def `{!BiInternalEq PROP} (A : ofeT) (a b : A) : monPred :=
   MonPred (λ _, a ≡ b)%I _.
-Definition monPred_internal_eq_aux `{!BiInternalEq PROP} : seal (@monPred_internal_eq_def _).
+Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def).
 Proof. by eexists. Qed.
-Definition monPred_internal_eq `{!BiInternalEq PROP} := monPred_internal_eq_aux.(unseal).
-Definition monPred_internal_eq_eq `{!BiInternalEq PROP} :
-  @internal_eq _ (@monPred_internal_eq _) = _ := monPred_internal_eq_aux.(seal_eq).
+Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
+Arguments monPred_internal_eq {_}.
+Lemma monPred_internal_eq_eq `{!BiInternalEq PROP} :
+  @internal_eq _ (@monPred_internal_eq _) = monPred_internal_eq_def.
+Proof. rewrite -monPred_internal_eq_aux.(seal_eq) //. Qed.
 
 Lemma monPred_internal_eq_mixin `{!BiInternalEq PROP} :
   BiInternalEqMixin monPredI (@monPred_internal_eq _).
@@ -861,10 +865,11 @@ Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
         (P : monPred) : monPred :=
   MonPred (λ i, |={E1,E2}=> P i)%I _.
 Next Obligation. solve_proper. Qed.
-Definition monPred_fupd_aux `{BiFUpd PROP} : seal monPred_fupd_def. Proof. by eexists. Qed.
-Definition monPred_fupd `{BiFUpd PROP} : FUpd _ := monPred_fupd_aux.(unseal).
-Definition monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = _ :=
-  monPred_fupd_aux.(seal_eq).
+Definition monPred_fupd_aux : seal (@monPred_fupd_def). Proof. by eexists. Qed.
+Definition monPred_fupd := monPred_fupd_aux.(unseal).
+Arguments monPred_fupd {_}.
+Lemma monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = monPred_fupd_def.
+Proof. rewrite -monPred_fupd_aux.(seal_eq) //. Qed.
 
 Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
 Proof.
@@ -898,9 +903,11 @@ Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
 (** Plainly *)
 Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
   MonPred (λ _, ∀ i, ■ (P i))%I _.
-Definition monPred_plainly_aux `{BiPlainly PROP} : seal monPred_plainly_def. Proof. by eexists. Qed.
-Definition monPred_plainly `{BiPlainly PROP} : Plainly _ := monPred_plainly_aux.(unseal).
-Definition monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = _ := monPred_plainly_aux.(seal_eq).
+Definition monPred_plainly_aux : seal (@monPred_plainly_def). Proof. by eexists. Qed.
+Definition monPred_plainly := monPred_plainly_aux.(unseal).
+Arguments monPred_plainly {_}.
+Lemma monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = monPred_plainly_def.
+Proof. rewrite -monPred_plainly_aux.(seal_eq) //. Qed.
 
 Lemma monPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin monPredI monPred_plainly.
 Proof.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 955235d00532d7250632be03ee651e5a17daf781..51604339186b0091c63e4276d418ec9fee047d3f 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -57,12 +57,14 @@ Proof.
     rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne.
 Qed.
 
-Definition twp_def `{!irisG Λ Σ} (s : stuckness) (E : coPset)
-    (e : expr Λ) (Φ : val Λ → iProp Σ) :
-  iProp Σ := bi_least_fixpoint (twp_pre' s) (E,e,Φ).
-Definition twp_aux `{!irisG Λ Σ} : seal (@twp_def Λ Σ _). Proof. by eexists. Qed.
-Instance twp' `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness := twp_aux.(unseal).
-Definition twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _ := twp_aux.(seal_eq).
+Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
+  := λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
+Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
+Definition twp' := twp_aux.(unseal).
+Arguments twp' {Λ Σ _}.
+Existing Instance twp'.
+Lemma twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _.
+Proof. rewrite -twp_aux.(seal_eq) //. Qed.
 
 Section twp.
 Context `{!irisG Λ Σ}.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index ec4ab9f47002fe3115cf7dbc5f4ae0e592d401e7..8c2cb8f9a26722508ea118e00d474a865a082306 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -44,11 +44,14 @@ Proof.
   repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
-Definition wp_def `{!irisG Λ Σ} (s : stuckness) :
-  coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
-Definition wp_aux `{!irisG Λ Σ} : seal (@wp_def Λ Σ _). Proof. by eexists. Qed.
-Instance wp' `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
-Definition wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
+Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
+  λ s : stuckness, fixpoint (wp_pre s).
+Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
+Definition wp' := wp_aux.(unseal).
+Arguments wp' {Λ Σ _}.
+Existing Instance wp'.
+Lemma wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
+Proof. rewrite -wp_aux.(seal_eq) //. Qed.
 
 Section wp.
 Context `{!irisG Λ Σ}.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 5e99d04ed75b0ef2298682bc1271d25fe854e541..d9eea54a46d00bb9b3e61d34eff3060c5cfe4d53 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -237,9 +237,9 @@ way, [iFresh] can simply be implemented by changing the goal from
 using the tactic [change_no_check]. This way, the generated proof term
 contains no additional steps for changing the counter.
 
-For all definitions below, we first define a version that take the two contexts
-[env_intuitionistic] and [env_spatial] as its arguments, and then lift these
-definitions that take the whole proof mode context [Δ : envs PROP]. This is
+We first define a version [pre_envs_entails] that takes the two contexts
+[env_intuitionistic] and [env_spatial] as its arguments. We seal this definition
+and then lift it to take the whole proof mode context [Δ : envs PROP]. This is
 crucial to make sure that the counter [env_counter] is not part of the seal. *)
 Record envs_wf' {PROP : bi} (Γp Γs : env PROP) := {
   env_intuitionistic_valid : env_wf Γp;
@@ -257,15 +257,19 @@ Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
 Instance: Params (@of_envs) 1 := {}.
 Arguments of_envs : simpl never.
 
-Definition envs_entails_aux :
-  seal (λ (PROP : bi) (Γp Γs : env PROP) (Q : PROP), of_envs' Γp Γs ⊢ Q).
-Proof. by eexists. Qed.
+Definition pre_envs_entails_def {PROP : bi} (Γp Γs : env PROP) (Q : PROP) :=
+  of_envs' Γp Γs ⊢ Q.
+Definition pre_envs_entails_aux : seal (@pre_envs_entails_def). Proof. by eexists. Qed.
+Definition pre_envs_entails := pre_envs_entails_aux.(unseal).
+Definition pre_envs_entails_eq : @pre_envs_entails = @pre_envs_entails_def :=
+  pre_envs_entails_aux.(seal_eq).
+
 Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
-  envs_entails_aux.(unseal) PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
+  pre_envs_entails  PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
 Definition envs_entails_eq :
   @envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
-Proof. by rewrite /envs_entails envs_entails_aux.(seal_eq). Qed.
-Arguments envs_entails {PROP} Δ Q%I : rename.
+Proof. by rewrite /envs_entails pre_envs_entails_eq. Qed.
+Arguments envs_entails {PROP} Δ Q%I.
 Instance: Params (@envs_entails) 1 := {}.
 
 Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {