diff --git a/theories/coPset.v b/theories/coPset.v
index 0212d629a447275ddcb0bb35f0ca2f4fa949939b..f8d4a230be858711e39b594c5f64fb482ba67cf4 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -183,8 +183,8 @@ Global Instance coPset_singleton : Singleton positive coPset := λ p,
   CoPset_ (coPset_singleton_raw p) (coPset_singleton_wf _).
 Global Instance coPset_elem_of : ElemOf positive coPset := λ p X,
   e_of p (coPset_car X).
-Global Instance coPset_empty : Empty coPset := CoPset_ (coPLeaf false) stt.
-Global Instance coPset_top : Top coPset := CoPset_ (coPLeaf true) stt.
+Global Instance coPset_empty : Empty coPset := CoPset_ (coPLeaf false) (squash I).
+Global Instance coPset_top : Top coPset := CoPset_ (coPLeaf true) (squash I).
 Global Instance coPset_union : Union coPset :=
   λ '(CoPset_ t1 Ht1) '(CoPset_ t2 Ht2),
     CoPset_ (t1 ∪ t2) (coPset_union_wf _ _ Ht1 Ht2).
@@ -359,7 +359,7 @@ Qed.
 
 (** * Conversion to and from gsets of positives *)
 Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf positive m.
-Proof. unfold gmap_wf. apply SIs_true_intro. by rewrite bool_decide_spec. Qed.
+Proof. by apply squash. Qed.
 Definition coPset_to_gset (X : coPset) : gset positive :=
   let 'Mapset m := coPset_to_Pset X in
   Mapset (GMap m (coPset_to_gset_wf m)).
diff --git a/theories/gmap.v b/theories/gmap.v
index 0808434891170934a96950ca6c5af5d88cc65acc..367889668ed3116a87f978350eddf2b9a2ff4cb0 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -21,7 +21,7 @@ Unset Default Proof Using.
 (** We pack a [Pmap] together with a proof that ensures that all keys correspond
 to codes of actual elements of the countable type. *)
 Definition gmap_wf K `{Countable K} {A} (m : Pmap A) : SProp :=
-  sprop_decide (map_Forall (λ p _, encode (A:=K) <$> decode p = Some p) m).
+  Squash (map_Forall (λ p _, encode (A:=K) <$> decode p = Some p) m).
 Record gmap K `{Countable K} A := GMap {
   gmap_car : Pmap A;
   gmap_prf : gmap_wf K gmap_car
@@ -42,7 +42,11 @@ Defined.
 (** * Operations on the data structure *)
 Global Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) :=
   λ i '(GMap m _), m !! encode i.
-Global Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ stt.
+
+Lemma gmap_empty_wf `{Countable K} {A} : gmap_wf (A:=A) K ∅.
+Proof. apply squash, map_Forall_empty. Qed.
+Global Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) :=
+  GMap ∅ gmap_empty_wf.
 (** Block reduction, even on concrete [gmap]s.
 Marking [gmap_empty] as [simpl never] would not be enough, because of
 https://github.com/coq/coq/issues/2972 and
@@ -51,10 +55,11 @@ And marking [gmap] consumers as [simpl never] does not work either, see:
 https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/171#note_53216
 *)
 Global Opaque gmap_empty.
+
 Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i :
   gmap_wf K m → gmap_wf K (partial_alter f (encode (A:=K) i) m).
 Proof.
-  intros Hm%sprop_decide_unpack. apply sprop_decide_pack.
+  intros Hm%(unsquash _). apply squash.
   intros p x. destruct (decide (encode i = p)) as [<-|?].
   - rewrite decode_encode; eauto.
   - rewrite lookup_partial_alter_ne by done. by apply Hm.
@@ -67,7 +72,7 @@ Global Instance gmap_partial_alter `{Countable K} {A} :
 Lemma gmap_fmap_wf `{Countable K} {A B} (f : A → B) m :
   gmap_wf K m → gmap_wf K (f <$> m).
 Proof.
-  intros Hm%sprop_decide_unpack. apply sprop_decide_pack.
+  intros Hm%(unsquash _). apply squash.
   intros p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto.
 Qed.
 Global Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f '(GMap m Hm),
@@ -75,7 +80,7 @@ Global Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f '(GMap m Hm
 Lemma gmap_omap_wf `{Countable K} {A B} (f : A → option B) m :
   gmap_wf K m → gmap_wf K (omap f m).
 Proof.
-  intros Hm%sprop_decide_unpack. apply sprop_decide_pack.
+  intros Hm%(unsquash _). apply squash.
   intros p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto.
 Qed.
 Global Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f '(GMap m Hm),
@@ -84,7 +89,7 @@ Lemma gmap_merge_wf `{Countable K} {A B C}
     (f : option A → option B → option C) m1 m2 :
   gmap_wf K m1 → gmap_wf K m2 → gmap_wf K (merge f m1 m2).
 Proof.
-  intros Hm1%sprop_decide_unpack Hm2%sprop_decide_unpack. apply sprop_decide_pack.
+  intros Hm1%(unsquash _) Hm2%(unsquash _). apply squash.
   intros p z. rewrite lookup_merge by done.
   destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
 Qed.
@@ -101,7 +106,7 @@ Proof.
   split.
   - unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
     apply gmap_eq, map_eq; intros i; simpl in *.
-    apply sprop_decide_unpack in Hm1; apply sprop_decide_unpack in Hm2.
+    apply (unsquash _) in Hm1; apply (unsquash _) in Hm2.
     apply option_eq; intros x; split; intros Hi.
     + pose proof (Hm1 i x Hi); simpl in *.
       by destruct (decode i); simplify_eq/=; rewrite <-Hm.
@@ -113,7 +118,7 @@ Proof.
     by contradict Hs; apply (inj encode).
   - intros A B f [m Hm] i; apply (lookup_fmap f m).
   - intros A [m Hm]; unfold map_to_list; simpl.
-    apply sprop_decide_unpack, map_Forall_to_list in Hm; revert Hm.
+    apply (unsquash _), map_Forall_to_list in Hm; revert Hm.
     induction (NoDup_map_to_list m) as [|[p x] l Hpx];
       inversion 1 as [|??? Hm']; simplify_eq/=; [by constructor|].
     destruct (decode p) as [i|] eqn:?; simplify_eq/=; constructor; eauto.
@@ -121,7 +126,7 @@ Proof.
     feed pose proof (proj1 (Forall_forall _ _) Hm' (p',x')); simpl in *; auto.
     by destruct (decode p') as [i'|]; simplify_eq/=.
   - intros A [m Hm] i x; unfold map_to_list, lookup; simpl.
-    apply sprop_decide_unpack in Hm; rewrite elem_of_list_omap; split.
+    apply (unsquash _) in Hm; rewrite elem_of_list_omap; split.
     + intros ([p' x']&Hp'&?); apply elem_of_map_to_list in Hp'.
       feed pose proof (Hm p' x'); simpl in *; auto.
       by destruct (decode p') as [i'|] eqn:?; simplify_eq/=.
diff --git a/theories/numbers.v b/theories/numbers.v
index 22a6dd9d2d498e0df2eb876ea9dd17dcb80a17d2..253a48971b2b476db3802095358072eda5a7c4c4 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -724,11 +724,11 @@ Local Close Scope Qc_scope.
 Definition Qp_red (q : positive * positive) : positive * positive :=
   (Pos.ggcd (q.1) (q.2)).2.
 Definition Qp_wf (q : positive * positive) : SProp :=
-  sprop_decide (Qp_red q = q).
+  Squash (Qp_red q = q).
 
 Lemma Qp_red_wf q : Qp_wf (Qp_red q).
 Proof.
-  apply sprop_decide_pack. unfold Qp_red. destruct q as [n d]; simpl.
+  apply squash. unfold Qp_red. destruct q as [n d]; simpl.
   pose proof (Pos.ggcd_greatest n d) as Hgreatest.
   destruct (Pos.ggcd n d) as [q [r1 r2]] eqn:?; simpl in *.
   pose proof (Pos.ggcd_correct_divisors r1 r2) as Hdiv.
@@ -789,7 +789,7 @@ Definition Qp_to_Q (q : Qp) : Q :=
 Lemma Qred_Qp_to_Q q : Qred (Qp_to_Q q) = Qp_to_Q q.
 Proof.
   destruct q as [[qn qd] Hq]; unfold Qred; simpl.
-  apply sprop_decide_unpack in Hq; unfold Qp_red in Hq; simpl in *.
+  apply (unsquash _) in Hq; unfold Qp_red in Hq; simpl in *.
   destruct (Pos.ggcd qn qd) as [? [??]]; by simplify_eq/=.
 Qed.
 Definition Qp_to_Qc (q : Qp) : Qc := Qcmake (Qp_to_Q q) (Qred_Qp_to_Q q).
@@ -894,7 +894,7 @@ Proof.
     by destruct (Pos.ggcd _ _) as [? [??]].
   - intros ->. destruct q as [[qn qd] Hq]; simpl.
     f_equal. unfold QP.
-    generalize (sprop_decide_unpack _ Hq). generalize (Qp_red_wf (qn, qd)).
+    generalize (unsquash _ Hq). generalize (Qp_red_wf (qn, qd)).
     generalize (Qp_red (qn, qd)). by intros ?? ->.
 Qed.
 
diff --git a/theories/pmap.v b/theories/pmap.v
index 73591c0cc361602577883119b2d6eab7f4d816e2..16425021b435d1f821ba2a9dcc6298a7ba08b58c 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -284,7 +284,7 @@ Global Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
   | right H => right (H ∘ proj1 (Pmap_eq m1 m2))
   end.
 
-Global Instance Pempty {A} : Empty (Pmap A) := PMap ∅ stt.
+Global Instance Pempty {A} : Empty (Pmap A) := PMap ∅ (squash I).
 Global Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
 Global Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) :=
   λ f i '(PMap t Ht),
diff --git a/theories/sprop.v b/theories/sprop.v
index d3c4e97f58ebeeeb2d5edd5229cd14538306fc75..edf9a73ca8d0a74f8e31af8c3b19579ea51540f7 100644
--- a/theories/sprop.v
+++ b/theories/sprop.v
@@ -2,17 +2,15 @@ From Coq Require Export Logic.StrictProp.
 From stdpp Require Import decidable.
 From stdpp Require Import options.
 
-Definition SIs_true (b: bool): SProp := if b then sUnit else sEmpty.
+Lemma unsquash (P : Prop) `{!Decision P} : Squash P → P.
+Proof.
+  intros HP. destruct (decide P) as [?|HnotP]; [assumption|].
+  assert sEmpty as []. destruct HP. destruct HnotP; assumption.
+Qed.
 
-Lemma SIs_true_intro {b: bool} : Is_true b → SIs_true b.
-Proof. destruct b; [constructor | intros []]. Qed.
-Lemma SIs_true_elim {b: bool} : SIs_true b → Is_true b.
-Proof. destruct b; simpl; [constructor | intros []]. Qed.
+Definition SIs_true (b : bool) : SProp := Squash (Is_true b).
 
-Definition sprop_decide (P : Prop) `{!Decision P} : SProp :=
-  SIs_true (bool_decide P).
-
-Lemma sprop_decide_pack (P : Prop) `{!Decision P} : P → sprop_decide P.
-Proof. intros HP. apply SIs_true_intro, bool_decide_pack, HP. Qed.
-Lemma sprop_decide_unpack (P : Prop) `{!Decision P} : sprop_decide P → P.
-Proof. intros HP. apply (bool_decide_unpack P), SIs_true_elim, HP. Qed.
+Lemma SIs_true_intro b : Is_true b → SIs_true b.
+Proof. apply squash. Qed.
+Lemma SIs_true_elim b : SIs_true b → Is_true b.
+Proof. apply (unsquash _). Qed.