diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 1d92cd555ef5a14fa7548a19c01254bb520ae222..7573f9c6acba0216cab16a2063d87b93f5f0fb4a 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -25,14 +25,11 @@ matching it against other forms of ownership. *)
 Definition heap_mapsto_def `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
   auth_own heap_name {[ l := Excl v ]}.
 (* Perform sealing *)
-Module Type HeapMapstoSig.
-  Parameter heap_mapsto : ∀ `{heapG Σ} (l : loc) (v: val), iPropG heap_lang Σ.
-  Axiom heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def.
-End HeapMapstoSig.
-Module Export HeapMapsto : HeapMapstoSig.
-  Definition heap_mapsto := @heap_mapsto_def.
-  Definition heap_mapsto_eq := Logic.eq_refl (@heap_mapsto).
-End HeapMapsto. 
+Definition heap_mapsto_aux : { x : _ & x = @heap_mapsto_def }.
+  exact (existT _ Logic.eq_refl). Qed.
+Definition heap_mapsto := projT1 heap_mapsto_aux.
+Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def := projT2 heap_mapsto_aux.
+Arguments heap_mapsto {_ _} _ _.
 
 Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
   ownP (of_heap h).
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 198b9c24c2ad59d77854fd2fb8c9fda580801f3d..c4a6805e4124d46dad4eb3a1ea4492511177c48b 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -16,14 +16,11 @@ Proof. split; try apply _. apply: inGF_inG. Qed.
 Definition auth_own_def `{authG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
   own γ (◯ a).
 (* Perform sealing *)
-Module Type AuthOwnSig.
-  Parameter auth_own : ∀ `{authG Λ Σ A} (γ : gname) (a : A), iPropG Λ Σ.
-  Axiom auth_own_eq : @auth_own = @auth_own_def.
-End AuthOwnSig.
-Module Export AuthOwn : AuthOwnSig.
-  Definition auth_own := @auth_own_def.
-  Definition auth_own_eq := Logic.eq_refl (@auth_own).
-End AuthOwn. 
+Definition auth_own_aux : { x : _ & x = @auth_own_def }.
+  exact (existT _ Logic.eq_refl). Qed.
+Definition auth_own := projT1 auth_own_aux.
+Definition auth_own_eq : @auth_own = @auth_own_def := projT2 auth_own_aux.
+Arguments auth_own {_ _ _ _ _} _ _.
 
 Definition auth_inv `{authG Λ Σ A}
     (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 1bda56082f5c579ae965ae2ced85e05b97742f87..56f63df963a2694a6a37dd9acf0df810df3e15d3 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -11,16 +11,12 @@ Proof. apply: inGF_inG. Qed.
 Definition saved_prop_own_def `{savedPropG Λ Σ}
     (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
   own γ (to_agree (Next (iProp_unfold P))).
-(* Perform sealing. *)
-Module Type SavedPropOwnSig.
-  Parameter saved_prop_own : ∀ `{savedPropG Λ Σ} (γ : gname) (P : iPropG Λ Σ),
-    iPropG Λ Σ.
-  Axiom saved_prop_own_eq : @saved_prop_own = @saved_prop_own_def.
-End SavedPropOwnSig.
-Module Export SavedPropOwn : SavedPropOwnSig.
-  Definition saved_prop_own := @saved_prop_own_def.
-  Definition saved_prop_own_eq := Logic.eq_refl (@saved_prop_own).
-End SavedPropOwn. 
+(* Perform sealing *)
+Definition saved_prop_own_aux : { x : _ & x = @saved_prop_own_def }.
+  exact (existT _ Logic.eq_refl). Qed.
+Definition saved_prop_own := projT1 saved_prop_own_aux.
+Definition saved_prop_own_eq : @saved_prop_own = @saved_prop_own_def := projT2 saved_prop_own_aux.
+Arguments saved_prop_own {_ _ _} _ _.
 Instance: Params (@saved_prop_own) 4.
 
 Section saved_prop.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 62696c3342771f7f8960be9b73e00c356ae23998..edc2938d401fa8d51dfaf0ba9c9a85d9b22018a2 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -16,24 +16,22 @@ Proof. split; try apply _. apply: inGF_inG. Qed.
 Definition sts_ownS_def `{i : stsG Λ Σ sts} (γ : gname)
            (S : sts.states sts) (T : sts.tokens sts) : iPropG Λ Σ:=
   own γ (sts_frag S T).
+(* Perform sealing. *)
+Definition sts_ownS_aux : { x : _ & x = @sts_ownS_def }.
+  exact (existT _ Logic.eq_refl). Qed.
+Definition sts_ownS := projT1 sts_ownS_aux.
+Definition sts_ownS_eq : @sts_ownS = @sts_ownS_def := projT2 sts_ownS_aux.
+Arguments sts_ownS {_ _ _ _} _ _ _.
+
 Definition sts_own_def `{i : stsG Λ Σ sts} (γ : gname)
            (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
   own γ (sts_frag_up s T).
 (* Perform sealing. *)
-Module Type StsOwnSig.
-  Parameter sts_ownS : ∀ `{i : stsG Λ Σ sts} (γ : gname)
-           (S : sts.states sts) (T : sts.tokens sts), iPropG Λ Σ.
-  Parameter sts_own : ∀ `{i : stsG Λ Σ sts} (γ : gname)
-           (s : sts.state sts) (T : sts.tokens sts), iPropG Λ Σ.
-  Axiom sts_ownS_eq : @sts_ownS = @sts_ownS_def.
-  Axiom sts_own_eq : @sts_own = @sts_own_def.
-End StsOwnSig.
-Module Export StsOwn : StsOwnSig.
-  Definition sts_ownS := @sts_ownS_def.
-  Definition sts_own := @sts_own_def.
-  Definition sts_ownS_eq := Logic.eq_refl (@sts_ownS_def).
-  Definition sts_own_eq := Logic.eq_refl (@sts_own_def).
-End StsOwn. 
+Definition sts_own_aux : { x : _ & x = @sts_own_def }.
+  exact (existT _ Logic.eq_refl). Qed.
+Definition sts_own := projT1 sts_own_aux.
+Definition sts_own_eq : @sts_own = @sts_own_def := projT2 sts_own_aux.
+Arguments sts_own {_ _ _ _} _ _ _.
 
 Definition sts_inv `{i : stsG Λ Σ sts} (γ : gname)
            (φ : sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=