diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 2bf1994a949ff44ca6dcc9e87d63e0778d0a6681..d31ec3f44fa5e75cde4cc4ca31d1b568baee4fba 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -25,11 +25,10 @@ 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 *)
-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_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
+Definition heap_mapsto {Σ h} := proj1_sig heap_mapsto_aux Σ h.
+Definition heap_mapsto_eq :
+  @heap_mapsto = @heap_mapsto_def := proj2_sig heap_mapsto_aux.
 
 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 90d5d6e455a677114125b053c8e32d4baac6f9ca..15f435ff598bfb45902563395ca84190867f6e7e 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -16,11 +16,9 @@ Proof. split; try apply _. apply: inGF_inG. Qed.
 Definition auth_own_def `{authG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
   own γ (◯ a).
 (* Perform sealing *)
-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_own_aux : { x | x = @auth_own_def }. by eexists. Qed.
+Definition auth_own {Λ Σ A Ae a} := proj1_sig auth_own_aux Λ Σ A Ae a.
+Definition auth_own_eq : @auth_own = @auth_own_def := proj2_sig auth_own_aux.
 
 Definition auth_inv `{authG Λ Σ A}
     (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 56f63df963a2694a6a37dd9acf0df810df3e15d3..b7254b5916f526f66c8d2efbc3ecd1d9cbf3b9d8 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -12,11 +12,11 @@ Definition saved_prop_own_def `{savedPropG Λ Σ}
     (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
   own γ (to_agree (Next (iProp_unfold P))).
 (* 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 {_ _ _} _ _.
+Definition saved_prop_own_aux : { x | x = @saved_prop_own_def }. by eexists. Qed.
+Definition saved_prop_own {Λ Σ s} := proj1_sig saved_prop_own_aux Λ Σ s.
+Definition saved_prop_own_eq :
+  @saved_prop_own = @saved_prop_own_def := proj2_sig saved_prop_own_aux.
+
 Instance: Params (@saved_prop_own) 4.
 
 Section saved_prop.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index edc2938d401fa8d51dfaf0ba9c9a85d9b22018a2..8c9480ab5faba851911dee3378a615f93098aee0 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -14,30 +14,26 @@ Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
 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 Λ Σ:=
+    (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_ownS_aux : { x | x = @sts_ownS_def }. by eexists. Qed.
+Definition sts_ownS {Λ Σ sts i} := proj1_sig sts_ownS_aux Λ Σ sts i.
+Definition sts_ownS_eq : @sts_ownS = @sts_ownS_def := proj2_sig sts_ownS_aux.
 
 Definition sts_own_def `{i : stsG Λ Σ sts} (γ : gname)
-           (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
+    (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
   own γ (sts_frag_up s T).
 (* Perform sealing. *)
-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_own_aux : { x | x = @sts_own_def }. by eexists. Qed.
+Definition sts_own {Λ Σ sts i} := proj1_sig sts_own_aux Λ Σ sts i.
+Definition sts_own_eq : @sts_own = @sts_own_def := proj2_sig sts_own_aux.
 
 Definition sts_inv `{i : stsG Λ Σ sts} (γ : gname)
-           (φ : sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
+    (φ : sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
   (∃ s, own γ (sts_auth s ∅) ★ φ s)%I.
 Definition sts_ctx `{i : stsG Λ Σ sts} (γ : gname)
-           (N : namespace) (φ: sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
+    (N : namespace) (φ: sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
   inv N (sts_inv γ φ).
 
 Instance: Params (@sts_inv) 5.