diff --git a/CHANGELOG.md b/CHANGELOG.md
index 83f4cb9b0128374b9ce0668be0f59e60f8b7e8a7..e99dd0119d5f3434c39bd207f5671f391f4be5ec 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -162,6 +162,14 @@ API-breaking change is listed.
 - Make `Forall2_nil`, `Forall2_cons` bidirectional lemmas with `Forall2_nil_2`,
   `Forall2_cons_2` being the original one-directional versions (matching
   `Forall_nil` and `Forall_cons`). Rename `Forall2_cons_inv` to `Forall2_cons_1`.
+- Use `SProp` in the implementation of `pmap`, `gmap`, `gset`, `Qp`, and
+  `coPset`. This ensures that more equalities hold definitionally, and can thus
+  be proved by `reflexivity` or even by conversion as part of unification.
+  For example `1/4 + 3/4 = 1`, or `{[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]}`,
+  or `{[ 1 ]} ∖ {[ 1 ]} = ∅` hold definitionally. As part of this change, add
+  some basic infrastructure for `SProp`: the definition `SIs_true`, and the
+  lemmas `SIs_true_intro`, `SIs_true_elim`, and `unsquash`. The APIs of the
+  aforementioned data structures should be unaffected.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/README.md b/README.md
index 756147569f5d71672ea6175b5daa9f13e10c5695..afe795b00ab28851dc9fda41644148a01316529a 100644
--- a/README.md
+++ b/README.md
@@ -40,6 +40,9 @@ Notably:
   [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
   becomes unreliable. We do not consider this an issue since we use `lia` (for
   which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
+* `Set Allow StrictProp`: the type of strict propositions (`SProp`) is enabled
+  by default since Coq 8.12. To make prior versions of Coq happy we need to
+  allow it explicitly.
 
 ## Prerequisites
 
diff --git a/tests/gmap.ref b/tests/gmap.ref
index a4d42549233b5c0153c1b455eb21f2651d09f7d4..7e6c436b2490f2d6f417c76ba2c4ea110f04263c 100644
--- a/tests/gmap.ref
+++ b/tests/gmap.ref
@@ -70,3 +70,23 @@ Failed to progress.
   
   ============================
   bool_decide (∅ ⊆ {[1; 2; 3]}) = true
+"pmap_insert_positives_test"
+     : string
+     = true
+     : bool
+"gmap_insert_positives_test"
+     : string
+     = true
+     : bool
+"gmap_insert_comm"
+     : string
+1 goal
+  
+  ============================
+  {[3 := false; 2 := true]} = {[2 := true; 3 := false]}
+"gmap_lookup_concrete"
+     : string
+1 goal
+  
+  ============================
+  {[3 := false; 2 := true]} !! 2 = Some true
diff --git a/tests/gmap.v b/tests/gmap.v
index 6cb7029b63ea9553c3255497fe63bd09b68fb38d..158b665c085c2fe25dc075f067303d9265647c73 100644
--- a/tests/gmap.v
+++ b/tests/gmap.v
@@ -1,4 +1,4 @@
-From stdpp Require Import gmap.
+From stdpp Require Import strings pmap gmap.
 
 Goal {[1; 2; 3]} =@{gset nat} ∅.
 Proof.
@@ -68,3 +68,90 @@ Proof.
   Show.
   reflexivity.
 Qed.
+
+Definition pmap_insert_positives (n : positive) : Pmap unit :=
+  Pos.iter (λ rec p m,
+    rec (p + 1)%positive (<[p:=tt]> m)) (λ _ m, m) n 1%positive ∅.
+Definition pmap_insert_positives_rev (n : positive) : Pmap unit :=
+  Pos.iter (λ rec p m,
+    rec (p - 1)%positive (<[p:=tt]> m)) (λ _ m, m) n n ∅.
+
+Definition pmap_insert_positives_test (p : positive) : bool :=
+  bool_decide (pmap_insert_positives p = pmap_insert_positives_rev p).
+
+(* Test that the time is approximately n-log-n. We cannot test this on CI since
+you get different timings all the time. Instead we just test for [256000], which
+likely takes forever if the complexity is not n-log-n. *)
+(*
+Time Eval vm_compute in pmap_insert_positives_test 1000.
+Time Eval vm_compute in pmap_insert_positives_test 2000.
+Time Eval vm_compute in pmap_insert_positives_test 4000.
+Time Eval vm_compute in pmap_insert_positives_test 8000.
+Time Eval vm_compute in pmap_insert_positives_test 16000.
+Time Eval vm_compute in pmap_insert_positives_test 32000.
+Time Eval vm_compute in pmap_insert_positives_test 64000.
+Time Eval vm_compute in pmap_insert_positives_test 128000.
+Time Eval vm_compute in pmap_insert_positives_test 256000.
+Time Eval vm_compute in pmap_insert_positives_test 512000.
+Time Eval vm_compute in pmap_insert_positives_test 1000000.
+*)
+Check "pmap_insert_positives_test".
+Eval vm_compute in pmap_insert_positives_test 256000.
+
+Definition gmap_insert_positives (n : positive) : gmap positive unit :=
+  Pos.iter (λ rec p m,
+    rec (p + 1)%positive (<[p:=tt]> m)) (λ _ m, m) n 1%positive ∅.
+Definition gmap_insert_positives_rev (n : positive) : gmap positive unit :=
+  Pos.iter (λ rec p m,
+    rec (p - 1)%positive (<[p:=tt]> m)) (λ _ m, m) n n ∅.
+
+(* Test that the time increases linearly *)
+Definition gmap_insert_positives_test (p : positive) : bool :=
+  bool_decide (gmap_insert_positives p = gmap_insert_positives_rev p).
+
+(* Test that the time is approximately n-log-n. We cannot test this on CI since
+you get different timings all the time. Instead we just test for [256000], which
+likely takes forever if the complexity is not n-log-n. *)
+(*
+Time Eval vm_compute in gmap_insert_positives_test 1000.
+Time Eval vm_compute in gmap_insert_positives_test 2000.
+Time Eval vm_compute in gmap_insert_positives_test 4000.
+Time Eval vm_compute in gmap_insert_positives_test 8000.
+Time Eval vm_compute in gmap_insert_positives_test 16000.
+Time Eval vm_compute in gmap_insert_positives_test 32000.
+Time Eval vm_compute in gmap_insert_positives_test 64000.
+Time Eval vm_compute in gmap_insert_positives_test 128000.
+Time Eval vm_compute in gmap_insert_positives_test 256000.
+Time Eval vm_compute in gmap_insert_positives_test 512000.
+Time Eval vm_compute in gmap_insert_positives_test 1000000.
+*)
+Check "gmap_insert_positives_test".
+Eval vm_compute in gmap_insert_positives_test 256000.
+
+Check "gmap_insert_comm".
+Theorem gmap_insert_comm :
+  {[ 3:=false; 2:=true]} =@{gmap nat bool} {[ 2:=true; 3:=false ]}.
+Proof. simpl. Show. reflexivity. Qed.
+
+Check "gmap_lookup_concrete".
+Theorem gmap_lookup_concrete :
+  lookup (M:=gmap nat bool) 2 {[ 3:=false; 2:=true ]} = Some true.
+Proof. simpl. Show. reflexivity. Qed.
+
+Theorem gmap_insert_positives_reflexivity_500 :
+  gmap_insert_positives 500 = gmap_insert_positives_rev 500.
+Proof. reflexivity. Qed.
+Theorem gmap_insert_positives_reflexivity_1000 :
+  gmap_insert_positives 1000 = gmap_insert_positives_rev 1000.
+Proof. (* this should take about a second *) reflexivity. Qed.
+
+Theorem gmap_insert_positives_union_reflexivity_500 :
+  (gmap_insert_positives_rev 400) ∪
+    (gmap_insert_positives 500 ∖ gmap_insert_positives_rev 400)
+  = gmap_insert_positives 500.
+Proof. reflexivity. Qed.
+Theorem gmap_insert_positives_union_reflexivity_1000 :
+  (gmap_insert_positives_rev 800) ∪
+    (gmap_insert_positives 1000 ∖ gmap_insert_positives_rev 800)
+  = gmap_insert_positives 1000.
+Proof. reflexivity. Qed.
diff --git a/theories/base.v b/theories/base.v
index ad373c01bc50804cd42e3ff8d973aaaed35964ea..b8bc0b8fc91594aa065c54f6b7ad6193e7924c8c 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -10,6 +10,7 @@ we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
 over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
 From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
 From Coq Require Import Permutation.
+From Coq Require Export Logic.StrictProp.
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 From stdpp Require Import options.
@@ -49,6 +50,10 @@ Obligation Tactic := idtac.
 (** 3. Hide obligations from the results of the [Search] commands. *)
 Add Search Blacklist "_obligation_".
 
+(** 4. [StrictProp] is enabled by default since Coq 8.12. To make prior versions
+of Coq happy we need to allow it explicitly. *)
+Global Set Allow StrictProp.
+
 (** * Sealing off definitions *)
 Section seal.
   Local Set Primitive Projections.
@@ -645,6 +650,21 @@ Proof. destruct b; simpl; tauto. Qed.
 Lemma Is_true_false (b : bool) : b = false → ¬b.
 Proof. now intros -> ?. Qed.
 
+(** ** SProp *)
+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.
+
+Definition SIs_true (b : bool) : SProp := Squash (Is_true b).
+
+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. destruct b; [left|right]; simpl; tauto. Qed.
+
+
 (** ** Unit *)
 Global Instance unit_equiv : Equiv unit := λ _ _, True.
 Global Instance unit_equivalence : Equivalence (≡@{unit}).
diff --git a/theories/coPset.v b/theories/coPset.v
index 8e8cb978c846d563b3c6c2042efe6805cecea937..f8d4a230be858711e39b594c5f64fb482ba67cf4 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -68,7 +68,7 @@ Proof.
   assert (r = coPLeaf b) as -> by (apply IHr; try apply (λ p, Ht (p~1)); eauto).
   by destruct b.
 Qed.
-Lemma coPset_eq t1 t2 :
+Lemma coPset_wf_eq t1 t2 :
   (∀ p, e_of p t1 = e_of p t2) → coPset_wf t1 → coPset_wf t2 → t1 = t2.
 Proof.
   revert t2.
@@ -115,15 +115,26 @@ Fixpoint coPset_opp_raw (t : coPset_raw) : coPset_raw :=
   | coPNode b l r => coPNode' (negb b) (coPset_opp_raw l) (coPset_opp_raw r)
   end.
 
-Lemma coPset_singleton_wf p : coPset_wf (coPset_singleton_raw p).
-Proof. induction p; simpl; eauto. Qed.
-Lemma coPset_union_wf t1 t2 : coPset_wf t1 → coPset_wf t2 → coPset_wf (t1 ∪ t2).
-Proof. revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto. Qed.
+Lemma coPset_singleton_wf p : SIs_true (coPset_wf (coPset_singleton_raw p)).
+Proof. apply SIs_true_intro. induction p; simpl; eauto. Qed.
+Lemma coPset_union_wf t1 t2 :
+  SIs_true (coPset_wf t1) → SIs_true (coPset_wf t2) →
+  SIs_true (coPset_wf (t1 ∪ t2)).
+Proof.
+  intros Hwf1%SIs_true_elim Hwf2%SIs_true_elim.
+  apply SIs_true_intro. revert Hwf1 Hwf2.
+  revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto.
+Qed.
 Lemma coPset_intersection_wf t1 t2 :
-  coPset_wf t1 → coPset_wf t2 → coPset_wf (t1 ∩ t2).
-Proof. revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto. Qed.
-Lemma coPset_opp_wf t : coPset_wf (coPset_opp_raw t).
-Proof. induction t as [[]|[]]; simpl; eauto. Qed.
+  SIs_true (coPset_wf t1) → SIs_true (coPset_wf t2) →
+  SIs_true (coPset_wf (t1 ∩ t2)).
+Proof.
+  intros Hwf1%SIs_true_elim Hwf2%SIs_true_elim.
+  apply SIs_true_intro. revert Hwf1 Hwf2.
+  revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto.
+Qed.
+Lemma coPset_opp_wf t : SIs_true (coPset_wf (coPset_opp_raw t)).
+Proof. apply SIs_true_intro. induction t as [[]|[]]; simpl; eauto. Qed.
 Lemma coPset_elem_of_singleton p q : e_of p (coPset_singleton_raw q) ↔ p = q.
 Proof.
   split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node].
@@ -150,22 +161,40 @@ Proof.
 Qed.
 
 (** * Packed together + set operations *)
-Definition coPset := { t | coPset_wf t }.
+(** Add an underscore to [CoPset_] to avoid nameclash with Iris's
+[algebra.coPset.CoPset]. *)
+Record coPset := CoPset_ {
+  coPset_car : coPset_raw;
+  coPset_prf : SIs_true (coPset_wf coPset_car);
+}.
+
+Lemma coPset_eq (X1 X2 : coPset) : X1 = X2 ↔ coPset_car X1 = coPset_car X2.
+Proof.
+  split; [by intros ->|intros].
+  destruct X1 as [t1 ?], X2 as [t2 ?]; by simplify_eq/=.
+Qed.
+Global Instance coPset_eq_dec : EqDecision coPset := λ X1 X2,
+  match coPset_raw_eq_dec (coPset_car X1) (coPset_car X2) with
+  | left H => left (proj2 (coPset_eq X1 X2) H)
+  | right H => right (H ∘ proj1 (coPset_eq X1 X2))
+  end.
 
 Global Instance coPset_singleton : Singleton positive coPset := λ p,
-  coPset_singleton_raw p ↾ coPset_singleton_wf _.
-Global Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
-Global Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
-Global Instance coPset_top : Top coPset := coPLeaf true ↾ I.
-Global Instance coPset_union : Union coPset := λ X Y,
-  let (t1,Ht1) := X in let (t2,Ht2) := Y in
-  (t1 ∪ t2) ↾ coPset_union_wf _ _ Ht1 Ht2.
-Global Instance coPset_intersection : Intersection coPset := λ X Y,
-  let (t1,Ht1) := X in let (t2,Ht2) := Y in
-  (t1 ∩ t2) ↾ coPset_intersection_wf _ _ Ht1 Ht2.
-Global Instance coPset_difference : Difference coPset := λ X Y,
-  let (t1,Ht1) := X in let (t2,Ht2) := Y in
-  (t1 ∩ coPset_opp_raw t2) ↾ coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
+  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) (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).
+Global Instance coPset_intersection : Intersection coPset :=
+  λ '(CoPset_ t1 Ht1) '(CoPset_ t2 Ht2),
+    CoPset_ (t1 ∩ t2) (coPset_intersection_wf _ _ Ht1 Ht2).
+Global Instance coPset_difference : Difference coPset :=
+  λ '(CoPset_ t1 Ht1) '(CoPset_ t2 Ht2),
+    CoPset_ (t1 ∩ coPset_opp_raw t2)
+           (coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _)).
 
 Global Instance coPset_top_set : TopSet positive coPset.
 Proof.
@@ -189,22 +218,22 @@ Global Hint Resolve coPset_top_subseteq : core.
 Global Instance coPset_leibniz : LeibnizEquiv coPset.
 Proof.
   intros X Y; rewrite set_equiv; intros HXY.
-  apply (sig_eq_pi _), coPset_eq; try apply @proj2_sig.
+  apply coPset_eq, coPset_wf_eq; [|apply SIs_true_elim, coPset_prf..].
   intros p; apply eq_bool_prop_intro, (HXY p).
 Qed.
-
 Global Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
 Proof. solve_decision. Defined.
 Global Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
-Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
+Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Qed.
 Global Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
 Proof.
- refine (λ X Y, cast_if (decide (X ∩ Y = ∅)));
-  abstract (by rewrite disjoint_intersection_L).
+  refine (λ X Y, cast_if (decide (X ∩ Y = ∅)));
+   abstract (by rewrite disjoint_intersection_L).
 Defined.
 Global Instance mapset_subseteq_dec : RelDecision (⊆@{coPset}).
 Proof.
- refine (λ X Y, cast_if (decide (X ∪ Y = Y))); abstract (by rewrite subseteq_union_L).
+  refine (λ X Y, cast_if (decide (X ∪ Y = Y)));
+    abstract (by rewrite subseteq_union_L).
 Defined.
 
 (** * Finite sets *)
@@ -215,7 +244,7 @@ Fixpoint coPset_finite (t : coPset_raw) : bool :=
 Lemma coPset_finite_node b l r :
   coPset_finite (coPNode' b l r) = coPset_finite l && coPset_finite r.
 Proof. by destruct b, l as [[]|], r as [[]|]. Qed.
-Lemma coPset_finite_spec X : set_finite X ↔ coPset_finite (`X).
+Lemma coPset_finite_spec X : set_finite X ↔ coPset_finite (coPset_car X).
 Proof.
   destruct X as [t Ht].
   unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.
@@ -234,7 +263,8 @@ Proof.
 Qed.
 Global Instance coPset_finite_dec (X : coPset) : Decision (set_finite X).
 Proof.
-  refine (cast_if (decide (coPset_finite (`X)))); by rewrite coPset_finite_spec.
+  refine (cast_if (decide (coPset_finite (coPset_car X))));
+    by rewrite coPset_finite_spec.
 Defined.
 
 (** * Pick element from infinite sets *)
@@ -252,7 +282,8 @@ Fixpoint coPpick_raw (t : coPset_raw) : option positive :=
      | Some i => Some (i~0) | None => (~1) <$> coPpick_raw r
      end
   end.
-Definition coPpick (X : coPset) : positive := default 1 (coPpick_raw (`X)).
+Definition coPpick (X : coPset) : positive :=
+  default 1 (coPpick_raw (coPset_car X)).
 
 Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i → e_of i t.
 Proof.
@@ -278,10 +309,15 @@ Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
   | coPNode false l r => PNode' None (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
   | coPNode true l r => PNode (Some ()) (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
   end.
-Lemma coPset_to_Pset_wf t : coPset_wf t → Pmap_wf (coPset_to_Pset_raw t).
-Proof. induction t as [|[]]; simpl; eauto using PNode_wf. Qed.
+Lemma coPset_to_Pset_wf t :
+  SIs_true (coPset_wf t) → SIs_true (Pmap_wf (coPset_to_Pset_raw t)).
+Proof.
+  intros Hwf%SIs_true_elim. apply SIs_true_intro.
+  induction t as [|[]]; simpl; eauto using PNode_wf.
+Qed.
 Definition coPset_to_Pset (X : coPset) : Pset :=
-  let (t,Ht) := X in Mapset (PMap (coPset_to_Pset_raw t) (coPset_to_Pset_wf _ Ht)).
+  let (t,Ht) := X in
+  Mapset (PMap (coPset_to_Pset_raw t) (coPset_to_Pset_wf _ Ht)).
 Lemma elem_of_coPset_to_Pset X i : set_finite X → i ∈ coPset_to_Pset X ↔ i ∈ X.
 Proof.
   rewrite coPset_finite_spec; destruct X as [t Ht].
@@ -297,8 +333,10 @@ Fixpoint Pset_to_coPset_raw (t : Pmap_raw ()) : coPset_raw :=
   | PNode None l r => coPNode false (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
   | PNode (Some _) l r => coPNode true (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
   end.
-Lemma Pset_to_coPset_wf t : Pmap_wf t → coPset_wf (Pset_to_coPset_raw t).
+Lemma Pset_to_coPset_wf t :
+  SIs_true (Pmap_wf t) → SIs_true (coPset_wf (Pset_to_coPset_raw t)).
 Proof.
+  intros Hwf%SIs_true_elim. apply SIs_true_intro. revert Hwf.
   induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto.
   - intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
   - destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
@@ -310,7 +348,8 @@ Lemma Pset_to_coPset_raw_finite t : coPset_finite (Pset_to_coPset_raw t).
 Proof. induction t as [|[[]|]]; simpl; rewrite ?andb_True; auto. Qed.
 
 Definition Pset_to_coPset (X : Pset) : coPset :=
-  let 'Mapset (PMap t Ht) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
+  let 'Mapset (PMap t Ht) := X in
+  CoPset_ (Pset_to_coPset_raw t) (Pset_to_coPset_wf _ Ht).
 Lemma elem_of_Pset_to_coPset X i : i ∈ Pset_to_coPset X ↔ i ∈ X.
 Proof. destruct X as [[t ?]]; apply elem_of_Pset_to_coPset_raw. Qed.
 Lemma Pset_to_coPset_finite X : set_finite (Pset_to_coPset X).
@@ -320,13 +359,14 @@ Qed.
 
 (** * Conversion to and from gsets of positives *)
 Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf positive m.
-Proof. unfold gmap_wf. 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)).
 
 Definition gset_to_coPset (X : gset positive) : coPset :=
-  let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
+  let 'Mapset (GMap (PMap t Ht) _) := X in
+  CoPset_ (Pset_to_coPset_raw t) (Pset_to_coPset_wf _ Ht).
 
 Lemma elem_of_coPset_to_gset X i : set_finite X → i ∈ coPset_to_gset X ↔ i ∈ X.
 Proof.
@@ -380,10 +420,10 @@ Fixpoint coPset_suffixes_raw (p : positive) : coPset_raw :=
   | p~0 => coPNode' false (coPset_suffixes_raw p) (coPLeaf false)
   | p~1 => coPNode' false (coPLeaf false) (coPset_suffixes_raw p)
   end.
-Lemma coPset_suffixes_wf p : coPset_wf (coPset_suffixes_raw p).
-Proof. induction p; simpl; eauto. Qed.
+Lemma coPset_suffixes_wf p : SIs_true (coPset_wf (coPset_suffixes_raw p)).
+Proof. apply SIs_true_intro. induction p; simpl; eauto. Qed.
 Definition coPset_suffixes (p : positive) : coPset :=
-  coPset_suffixes_raw p ↾ coPset_suffixes_wf _.
+  CoPset_ (coPset_suffixes_raw p) (coPset_suffixes_wf _).
 Lemma elem_coPset_suffixes p q : p ∈ coPset_suffixes q ↔ ∃ q', p = q' ++ q.
 Proof.
   unfold elem_of, coPset_elem_of; simpl; split.
@@ -411,14 +451,14 @@ Fixpoint coPset_r_raw (t : coPset_raw) : coPset_raw :=
   | coPNode b l r => coPNode' false (coPset_r_raw l) (coPset_r_raw r)
   end.
 
-Lemma coPset_l_wf t : coPset_wf (coPset_l_raw t).
-Proof. induction t as [[]|]; simpl; auto. Qed.
-Lemma coPset_r_wf t : coPset_wf (coPset_r_raw t).
-Proof. induction t as [[]|]; simpl; auto. Qed.
+Lemma coPset_l_wf t : SIs_true (coPset_wf (coPset_l_raw t)).
+Proof. apply SIs_true_intro. induction t as [[]|]; simpl; auto. Qed.
+Lemma coPset_r_wf t : SIs_true (coPset_wf (coPset_r_raw t)).
+Proof. apply SIs_true_intro.  induction t as [[]|]; simpl; auto. Qed.
 Definition coPset_l (X : coPset) : coPset :=
-  let (t,Ht) := X in coPset_l_raw t ↾ coPset_l_wf _.
+  let (t,Ht) := X in CoPset_ (coPset_l_raw t) (coPset_l_wf _).
 Definition coPset_r (X : coPset) : coPset :=
-  let (t,Ht) := X in coPset_r_raw t ↾ coPset_r_wf _.
+  let (t,Ht) := X in CoPset_ (coPset_r_raw t) (coPset_r_wf _).
 
 Lemma coPset_lr_disjoint X : coPset_l X ∩ coPset_r X = ∅.
 Proof.
diff --git a/theories/countable.v b/theories/countable.v
index d73d18c9f95e55b8d2c358b77ab73d1a73852cee..72eeb254780c08fa01ac58b946d064ea7cf7282e 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -273,13 +273,8 @@ Next Obligation.
 Qed.
 
 Global Program Instance Qp_countable : Countable Qp :=
-  inj_countable
-    Qp_to_Qc
-    (λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
-Next Obligation.
-  intros [p Hp]. unfold mguard, option_guard; simpl.
-  case_match; [|done]. f_equal. by apply Qp_to_Qc_inj_iff.
-Qed.
+  inj_countable Qp_to_Qc Qc_to_Qp _.
+Next Obligation. intros p. by apply Qc_to_Qp_Some. Qed.
 
 Global Program Instance fin_countable n : Countable (fin n) :=
   inj_countable
diff --git a/theories/gmap.v b/theories/gmap.v
index 97726848b7b816d38e1ffb547545094017bf71b6..367889668ed3116a87f978350eddf2b9a2ff4cb0 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -20,8 +20,8 @@ Unset Default Proof Using.
 (** * The data structure *)
 (** 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) : Prop :=
-  bool_decide (map_Forall (λ p _, encode (A:=K) <$> decode p = Some p) m).
+Definition gmap_wf K `{Countable K} {A} (m : Pmap A) : SProp :=
+  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
@@ -31,8 +31,7 @@ Global Arguments gmap_car {_ _ _ _} _ : assert.
 Lemma gmap_eq `{Countable K} {A} (m1 m2 : gmap K A) :
   m1 = m2 ↔ gmap_car m1 = gmap_car m2.
 Proof.
-  split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=.
-  f_equal; apply proof_irrel.
+  split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=; done.
 Qed.
 Global Instance gmap_eq_eq `{Countable K, EqDecision A} : EqDecision (gmap K A).
 Proof.
@@ -43,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 ∅ I.
+
+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
@@ -52,11 +55,12 @@ 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.
-  unfold gmap_wf; rewrite !bool_decide_spec.
-  intros Hm p x. destruct (decide (encode i = p)) as [<-|?].
+  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.
 Qed.
@@ -68,16 +72,16 @@ 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.
-  unfold gmap_wf; rewrite !bool_decide_spec.
-  intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto.
+  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),
   GMap (f <$> m) (gmap_fmap_wf f 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.
-  unfold gmap_wf; rewrite !bool_decide_spec.
-  intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto.
+  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),
   GMap (omap f m) (gmap_omap_wf f m Hm).
@@ -85,8 +89,8 @@ 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.
-  unfold gmap_wf; rewrite !bool_decide_spec.
-  intros Hm1 Hm2 p z. rewrite lookup_merge; intros.
+  intros Hm1%(unsquash _) Hm2%(unsquash _). apply squash.
+  intros p z. rewrite lookup_merge by done.
   destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
 Qed.
 Global Instance gmap_merge `{Countable K} : Merge (gmap K) :=
@@ -102,7 +106,7 @@ Proof.
   split.
   - unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
     apply gmap_eq, map_eq; intros i; simpl in *.
-    apply bool_decide_unpack in Hm1; apply bool_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.
@@ -114,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 bool_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.
@@ -122,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 bool_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/namespaces.v b/theories/namespaces.v
index 975d7f48fd73448c7e453b7e33b0b4bc58adc4f6..1d368be87957bb750270aebd81bad249b54965e8 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -36,7 +36,7 @@ Section namespace.
   Proof. intros N1 x1 N2 x2; rewrite !ndot_eq; naive_solver. Qed.
 
   Lemma nclose_nroot : ↑nroot = (⊤:coPset).
-  Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
+  Proof. by rewrite nclose_eq. Qed.
 
   Lemma nclose_subseteq N x : ↑N.@x ⊆ (↑N : coPset).
   Proof.
diff --git a/theories/numbers.v b/theories/numbers.v
index 9600f0fc46d6493dc07613f450e13acb954beb22..4c15f5a87029de829d71af737fba517bfafa13dc 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -721,77 +721,109 @@ Qed.
 Local Close Scope Qc_scope.
 
 (** * Positive rationals *)
-Declare Scope Qp_scope.
-Delimit Scope Qp_scope with Qp.
+(** We define the type [Qp] of positive rationals as fractions of positives with
+an [SProp]-based proof that ensures the fraction is in canonical form (i.e., its
+gcd is 1). Note that we do not define [Qp] as a subset (i.e., Sigma) of the
+standard library's [Qc] because the type [Qc] uses a [Prop]-based proof (not [SProp]) for canonicity
+of the fraction. *)
+Definition Qp_red (q : positive * positive) : positive * positive :=
+  (Pos.ggcd (q.1) (q.2)).2.
+Definition Qp_wf (q : positive * positive) : SProp :=
+  Squash (Qp_red q = q).
+
+Lemma Qp_red_wf q : Qp_wf (Qp_red q).
+Proof.
+  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.
+  destruct (Pos.ggcd r1 r2) as [q' [r1' r2']] eqn:?; simpl in *.
+  destruct Hdiv as [-> ->].
+  rewrite (Hgreatest q') by (by apply Pos.divide_mul_l, Z.divide_Zpos).
+  by rewrite !Pos.mul_1_l.
+Qed.
+
+Record Qp := QP' {
+  Qp_car : positive * positive;
+  Qp_prf : Qp_wf Qp_car;
+}.
+Definition QP (n d : positive) : Qp :=
+  QP' (Qp_red (n,d)) (Qp_red_wf _).
 
-Record Qp := mk_Qp { Qp_to_Qc : Qc ; Qp_prf : (0 < Qp_to_Qc)%Qc }.
 Add Printing Constructor Qp.
+
+Declare Scope Qp_scope.
+Delimit Scope Qp_scope with Qp.
 Bind Scope Qp_scope with Qp.
-Global Arguments Qp_to_Qc _%Qp : assert.
 
 Local Open Scope Qp_scope.
 
-Lemma Qp_to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q.
-Proof.
-  split; [|by intros ->].
-  destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _).
-Qed.
-Global Instance Qp_eq_dec : EqDecision Qp.
-Proof.
-  refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q)));
-    by rewrite <-Qp_to_Qc_inj_iff.
-Defined.
-
+(** ** Operations *)
 Definition Qp_add (p q : Qp) : Qp :=
-  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
-  mk_Qp (p + q) (Qcplus_pos_pos _ _ Hp Hq).
+  let '(QP' (pn,pd) _) := p in let '(QP' (qn,qd) _) := q in
+  QP (pn * qd + qn * pd) (pd * qd).
 Global Arguments Qp_add : simpl never.
 
 Definition Qp_sub (p q : Qp) : option Qp :=
-  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
-  let pq := (p - q)%Qc in
-  guard (0 < pq)%Qc as Hpq; Some (mk_Qp pq Hpq).
+  let '(QP' (pn,pd) _) := p in let '(QP' (qn,qd) _) := q in
+  guard (qn * pd < pn * qd)%positive;
+  Some (QP (pn * qd - qn * pd) (pd * qd)).
 Global Arguments Qp_sub : simpl never.
 
 Definition Qp_mul (p q : Qp) : Qp :=
-  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
-  mk_Qp (p * q) (Qcmult_pos_pos _ _ Hp Hq).
+  let '(QP' (pn,pd) _) := p in let '(QP' (qn,qd) _) := q in
+  QP (pn * qn) (pd * qd).
 Global Arguments Qp_mul : simpl never.
 
 Definition Qp_inv (q : Qp) : Qp :=
-  let 'mk_Qp q Hq := q return _ in
-  mk_Qp (/ q)%Qc (Qcinv_pos _ Hq).
+  let '(QP' (qn,qd) _) := q in
+  QP qd qn.
 Global Arguments Qp_inv : simpl never.
 
 Definition Qp_div (p q : Qp) : Qp := Qp_mul p (Qp_inv q).
 Typeclasses Opaque Qp_div.
 Global Arguments Qp_div : simpl never.
 
+Definition pos_to_Qp (n : positive) : Qp := QP n 1.
+Global Arguments pos_to_Qp : simpl never.
+
+Definition Qp_to_Q (q : Qp) : Q :=
+  let '(QP' (pn,pd) _) := q in
+  Qmake (Z.pos pn) pd.
+
+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 (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).
+
+Definition Qc_to_Qp (q : Qc) : option Qp :=
+  match q return _ with
+  | Qcmake (Qmake (Z.pos n) d) _ => Some (QP n d)
+  | _ => None
+  end.
+
+Definition Qp_le (p q : Qp) : Prop :=
+  let '(QP' (pn,pd) _) := p in let '(QP' (qn,qd) _) := q in
+  (pn * qd ≤ qn * pd)%positive.
+Definition Qp_lt (p q : Qp) : Prop :=
+  let '(QP' (pn,pd) _) := p in let '(QP' (qn,qd) _) := q in
+  (pn * qd < qn * pd)%positive.
+
+(** ** Notations *)
 Infix "+" := Qp_add : Qp_scope.
 Infix "-" := Qp_sub : Qp_scope.
 Infix "*" := Qp_mul : Qp_scope.
 Notation "/ q" := (Qp_inv q) : Qp_scope.
 Infix "/" := Qp_div : Qp_scope.
 
-Lemma Qp_to_Qc_inj_add p q : (Qp_to_Qc (p + q) = Qp_to_Qc p + Qp_to_Qc q)%Qc.
-Proof. by destruct p, q. Qed.
-Lemma Qp_to_Qc_inj_mul p q : (Qp_to_Qc (p * q) = Qp_to_Qc p * Qp_to_Qc q)%Qc.
-Proof. by destruct p, q. Qed.
-
-Program Definition pos_to_Qp (n : positive) : Qp := mk_Qp (Qc_of_Z $ Z.pos n) _.
-Next Obligation. intros n. by rewrite <-Z2Qc_inj_0, <-Z2Qc_inj_lt. Qed.
-Global Arguments pos_to_Qp : simpl never.
-
 Notation "1" := (pos_to_Qp 1) : Qp_scope.
 Notation "2" := (pos_to_Qp 2) : Qp_scope.
 Notation "3" := (pos_to_Qp 3) : Qp_scope.
 Notation "4" := (pos_to_Qp 4) : Qp_scope.
 
-Definition Qp_le (p q : Qp) : Prop :=
-  let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p ≤ q)%Qc.
-Definition Qp_lt (p q : Qp) : Prop :=
-  let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p < q)%Qc.
-
 Infix "≤" := Qp_le : Qp_scope.
 Infix "<" := Qp_lt : Qp_scope.
 Notation "p ≤ q ≤ r" := (p ≤ q ∧ q ≤ r) : Qp_scope.
@@ -804,56 +836,141 @@ Notation "(<)" := Qp_lt (only parsing) : Qp_scope.
 
 Global Hint Extern 0 (_ ≤ _)%Qp => reflexivity : core.
 
+(** ** Properties about the conversion to [Qc] *)
+(** After having proved these, we never break the [Qp] abstraction and derive
+all [Qp] properties from the corresponding properties for [Qc]. *)
+Lemma Qp_to_Qc_pos p : (0 < Qp_to_Qc p)%Qc.
+Proof. destruct p as [[pn pd] Hp]. unfold Qclt, Qlt; simpl; lia. Qed.
+Lemma Qp_to_Qc_inj_add p q : Qp_to_Qc (p + q) = (Qp_to_Qc p + Qp_to_Qc q)%Qc.
+Proof.
+  destruct p as [[pn pd] Hp], q as [[qn qd] Hq]; simpl. unfold Qp_add.
+  apply Qc_is_canon; simpl. unfold Qeq, Qp_red, Qred; simpl.
+  by destruct (Pos.ggcd _ _) as [? [??]].
+Qed.
+Lemma Qp_to_Qc_inj_sub p q :
+  Qp_to_Qc <$> (p - q) =
+    guard (Qp_to_Qc q < Qp_to_Qc p)%Qc; Some (Qp_to_Qc p - Qp_to_Qc q)%Qc.
+Proof.
+  destruct p as [[pn pd] Hp], q as [[qn qd] Hq]; simpl. unfold Qp_sub.
+  case_option_guard as Hpq; [|by rewrite option_guard_False].
+  rewrite option_guard_True by done; f_equal/=.
+  apply Qc_is_canon; simpl. rewrite (Qred_correct (- _)).
+  unfold Qeq, Qp_red, Qred; simpl.
+  replace (Z.pos pn * Z.pos qd + - Z.pos qn * Z.pos pd)%Z
+    with (Z.pos (pn * qd - qn * pd)) by lia; simpl.
+  by destruct (Pos.ggcd _ _) as [? [??]].
+Qed.
+Lemma Qp_to_Qc_inj_mul p q : Qp_to_Qc (p * q) = (Qp_to_Qc p * Qp_to_Qc q)%Qc.
+Proof.
+  destruct p as [[pn pd] Hp], q as [[qn qd] Hq]; simpl.
+  apply Qc_is_canon; simpl. unfold Qeq, Qp_red, Qred; simpl.
+  by destruct (Pos.ggcd _ _) as [? [??]].
+Qed.
+Lemma Qp_to_Qc_inj_inv p : Qp_to_Qc (/ p) = (/ Qp_to_Qc p)%Qc.
+Proof.
+  destruct p as [[pn pd] Hp].
+  apply Qc_is_canon; simpl. unfold Qeq, Qp_red, Qred; simpl.
+  by destruct (Pos.ggcd _ _) as [? [??]].
+Qed.
+Lemma Qp_to_Qc_inj_div p q : Qp_to_Qc (p / q) = (Qp_to_Qc p / Qp_to_Qc q)%Qc.
+Proof. unfold Qp_div. by rewrite Qp_to_Qc_inj_mul, Qp_to_Qc_inj_inv. Qed.
+Lemma Qp_to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q.
+Proof.
+  split; [|by intros ->].
+  destruct p as [[pn pd] Hp], q as [[qn qd] Hq]; simpl. by intros [= -> ->].
+Qed.
 Lemma Qp_to_Qc_inj_le p q : p ≤ q ↔ (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc.
-Proof. by destruct p, q. Qed.
+Proof. by destruct p as [[pn pd] ?], q as [[qn qd] ?]. Qed.
 Lemma Qp_to_Qc_inj_lt p q : p < q ↔ (Qp_to_Qc p < Qp_to_Qc q)%Qc.
-Proof. by destruct p, q. Qed.
+Proof. by destruct p as [[pn pd] ?], q as [[qn qd] ?]. Qed.
+Lemma Qp_to_Qc_pos_to_Qp n : Qp_to_Qc (pos_to_Qp n) = Qc_of_Z (Z.pos n).
+Proof.
+  apply Qc_is_canon. unfold Qeq. simpl. unfold Qp_red; simpl.
+  pose proof (Pos.ggcd_correct_divisors n 1) as Hdiv.
+  destruct (Pos.ggcd _ _) as [p [r1 r2]]; simpl in *.
+  destruct Hdiv as [-> ?].
+  rewrite (Pos.mul_eq_1_l p r2), (Pos.mul_eq_1_r p r2) by done. lia.
+Qed.
+Lemma Qc_to_Qp_Some p q : Qc_to_Qp p = Some q ↔ p = Qp_to_Qc q.
+Proof.
+  split.
+  - intros Hpq. destruct p as [[[|pn|] pd] Hp]; simplify_eq/=.
+    apply Qc_is_canon; simpl. rewrite <-Hp. unfold Qeq, Qp_red, Qred; simpl.
+    by destruct (Pos.ggcd _ _) as [? [??]].
+  - intros ->. destruct q as [[qn qd] Hq]; simpl.
+    f_equal. unfold QP.
+    generalize (unsquash _ Hq). generalize (Qp_red_wf (qn, qd)).
+    generalize (Qp_red (qn, qd)). by intros ?? ->.
+Qed.
 
+(** ** Basic type class instances *)
+Global Instance Qp_eq_dec : EqDecision Qp.
+Proof.
+  refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q)));
+    by rewrite <-Qp_to_Qc_inj_iff.
+Defined.
 Global Instance Qp_le_dec : RelDecision (≤).
 Proof.
   refine (λ p q, cast_if (decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc));
     by rewrite Qp_to_Qc_inj_le.
-Qed.
+Defined.
 Global Instance Qp_lt_dec : RelDecision (<).
 Proof.
   refine (λ p q, cast_if (decide (Qp_to_Qc p < Qp_to_Qc q)%Qc));
     by rewrite Qp_to_Qc_inj_lt.
-Qed.
+Defined.
 Global Instance Qp_lt_pi p q : ProofIrrel (p < q).
-Proof. destruct p, q; apply _. Qed.
+Proof.
+  destruct p as [[pn pd] ?], q as [[qn qd] ?]. unfold Qp_lt, Pos.lt. apply _.
+Qed.
+
+Global Instance Qp_inhabited : Inhabited Qp := populate 1.
 
+(** ** Lattice structure *)
 Definition Qp_max (q p : Qp) : Qp := if decide (q ≤ p) then p else q.
 Definition Qp_min (q p : Qp) : Qp := if decide (q ≤ p) then q else p.
 
 Infix "`max`" := Qp_max : Qp_scope.
 Infix "`min`" := Qp_min : Qp_scope.
 
-Global Instance Qp_inhabited : Inhabited Qp := populate 1.
-
+(** ** Algebraic properties *)
 Global Instance Qp_add_assoc : Assoc (=) Qp_add.
-Proof. intros [p ?] [q ?] [r ?]; apply Qp_to_Qc_inj_iff, Qcplus_assoc. Qed.
+Proof.
+  intros p q r. apply Qp_to_Qc_inj_iff.
+  by rewrite !Qp_to_Qc_inj_add, Qcplus_assoc.
+Qed.
 Global Instance Qp_add_comm : Comm (=) Qp_add.
-Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcplus_comm. Qed.
+Proof.
+  intros p q. apply Qp_to_Qc_inj_iff.
+  by rewrite !Qp_to_Qc_inj_add, Qcplus_comm.
+Qed.
 Global Instance Qp_add_inj_r p : Inj (=) (=) (Qp_add p).
 Proof.
-  destruct p as [p ?].
-  intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (Qcplus p)).
+  intros q1 q2. rewrite <-!Qp_to_Qc_inj_iff, !Qp_to_Qc_inj_add.
+  apply (inj (Qcplus (Qp_to_Qc p))).
 Qed.
 Global Instance Qp_add_inj_l p : Inj (=) (=) (λ q, q + p).
 Proof.
-  destruct p as [p ?].
-  intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (λ q, q + p)%Qc).
+  intros q1 q2. rewrite <-!Qp_to_Qc_inj_iff, !Qp_to_Qc_inj_add.
+  apply (inj (λ q, q + Qp_to_Qc p)%Qc).
 Qed.
 
 Global Instance Qp_mul_assoc : Assoc (=) Qp_mul.
-Proof. intros [p ?] [q ?] [r ?]. apply Qp_to_Qc_inj_iff, Qcmult_assoc. Qed.
+Proof.
+  intros p q r. apply Qp_to_Qc_inj_iff.
+  by rewrite !Qp_to_Qc_inj_mul, Qcmult_assoc.
+Qed.
 Global Instance Qp_mul_comm : Comm (=) Qp_mul.
-Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcmult_comm. Qed.
+Proof.
+  intros p q. apply Qp_to_Qc_inj_iff.
+  by rewrite !Qp_to_Qc_inj_mul, Qcmult_comm.
+Qed.
 Global Instance Qp_mul_inj_r p : Inj (=) (=) (Qp_mul p).
 Proof.
-  destruct p as [p ?]. intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl.
+  intros q1 q2. rewrite <-!Qp_to_Qc_inj_iff, !Qp_to_Qc_inj_mul.
   intros Hpq.
-  apply (anti_symm Qcle); apply (Qcmult_le_mono_pos_l _ _ p); by rewrite ?Hpq.
+  apply (anti_symm Qcle); apply (Qcmult_le_mono_pos_l _ _ (Qp_to_Qc p));
+    first [apply Qp_to_Qc_pos|by rewrite Hpq].
 Qed.
 Global Instance Qp_mul_inj_l p : Inj (=) (=) (λ q, q * p).
 Proof.
@@ -861,23 +978,31 @@ Proof.
 Qed.
 
 Lemma Qp_mul_add_distr_l p q r : p * (q + r) = p * q + p * r.
-Proof. destruct p, q, r; by apply Qp_to_Qc_inj_iff, Qcmult_plus_distr_r. Qed.
+Proof.
+  by rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_add,
+    !Qp_to_Qc_inj_mul, Qp_to_Qc_inj_add, Qcmult_plus_distr_r.
+Qed.
 Lemma Qp_mul_add_distr_r p q r : (p + q) * r = p * r + q * r.
-Proof. destruct p, q, r; by apply Qp_to_Qc_inj_iff, Qcmult_plus_distr_l. Qed.
+Proof.
+  by rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_add,
+    !Qp_to_Qc_inj_mul, Qp_to_Qc_inj_add, Qcmult_plus_distr_l.
+Qed.
 Lemma Qp_mul_1_l p : 1 * p = p.
-Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_l. Qed.
+Proof. rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_mul. apply Qcmult_1_l. Qed.
 Lemma Qp_mul_1_r p : p * 1 = p.
-Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_r. Qed.
+Proof. rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_mul. apply Qcmult_1_r. Qed.
 
 Lemma Qp_1_1 : 1 + 1 = 2.
-Proof. compute_done. Qed.
+Proof. done. Qed.
 Lemma Qp_add_diag p : p + p = 2 * p.
 Proof. by rewrite <-Qp_1_1, Qp_mul_add_distr_r, !Qp_mul_1_l. Qed.
 
 Lemma Qp_mul_inv_l p : /p * p = 1.
 Proof.
-  destruct p as [p ?]; apply Qp_to_Qc_inj_iff; simpl.
-  by rewrite Qcmult_inv_l, Z2Qc_inj_1 by (by apply not_symmetry, Qclt_not_eq).
+  rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_mul, Qp_to_Qc_inj_inv.
+  assert (Qp_to_Qc p ≠ 0)%Qc.
+  { apply not_symmetry, Qclt_not_eq, Qp_to_Qc_pos. }
+  rewrite Qcmult_inv_l by done. by apply Qc_is_canon.
 Qed.
 Lemma Qp_mul_inv_r p : p * /p = 1.
 Proof. by rewrite (comm_L Qp_mul), Qp_mul_inv_l. Qed.
@@ -898,11 +1023,11 @@ Proof.
   by rewrite Qp_mul_inv_l, Hp, Qp_mul_inv_l.
 Qed.
 Lemma Qp_inv_1 : /1 = 1.
-Proof. compute_done. Qed.
+Proof. done. Qed.
 Lemma Qp_inv_half_half : /2 + /2 = 1.
-Proof. compute_done. Qed.
+Proof. done. Qed.
 Lemma Qp_inv_quarter_quarter : /4 + /4 = /2.
-Proof. compute_done. Qed.
+Proof. done. Qed.
 
 Lemma Qp_div_diag p : p / p = 1.
 Proof. apply Qp_mul_inv_r. Qed.
@@ -931,13 +1056,13 @@ Qed.
 Lemma Qp_div_2_mul p q : p / (2 * q) + p / (2 * q) = p / q.
 Proof. by rewrite <-Qp_div_add_distr, Qp_add_diag, Qp_div_mul_cancel_l. Qed.
 Lemma Qp_half_half : 1 / 2 + 1 / 2 = 1.
-Proof. compute_done. Qed.
+Proof. done. Qed.
 Lemma Qp_quarter_quarter : 1 / 4 + 1 / 4 = 1 / 2.
-Proof. compute_done. Qed.
+Proof. done. Qed.
 Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1.
-Proof. compute_done. Qed.
+Proof. done. Qed.
 Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1.
-Proof. compute_done. Qed.
+Proof. done. Qed.
 Global Instance Qp_div_inj_r p : Inj (=) (=) (Qp_div p).
 Proof. unfold Qp_div; apply _. Qed.
 Global Instance Qp_div_inj_l p : Inj (=) (=) (λ q, q / p)%Qp.
@@ -989,7 +1114,7 @@ Proof.
 Qed.
 
 Lemma Qp_add_le_mono_l p q r : p ≤ q ↔ r + p ≤ r + q.
-Proof. rewrite !Qp_to_Qc_inj_le. destruct p, q, r; apply Qcplus_le_mono_l. Qed.
+Proof. by rewrite !Qp_to_Qc_inj_le, !Qp_to_Qc_inj_add, <-Qcplus_le_mono_l. Qed.
 Lemma Qp_add_le_mono_r p q r : p ≤ q ↔ p + r ≤ q + r.
 Proof. rewrite !(comm_L Qp_add _ r). apply Qp_add_le_mono_l. Qed.
 Lemma Qp_add_le_mono q p n m : q ≤ n → p ≤ m → q + p ≤ n + m.
@@ -1004,7 +1129,8 @@ Proof. intros. etrans; [by apply Qp_add_lt_mono_l|by apply Qp_add_lt_mono_r]. Qe
 
 Lemma Qp_mul_le_mono_l p q r : p ≤ q ↔ r * p ≤ r * q.
 Proof.
-  rewrite !Qp_to_Qc_inj_le. destruct p, q, r; by apply Qcmult_le_mono_pos_l.
+  assert (0 < Qp_to_Qc r)%Qc by apply Qp_to_Qc_pos.
+  by rewrite !Qp_to_Qc_inj_le, !Qp_to_Qc_inj_mul, <-Qcmult_le_mono_pos_l.
 Qed.
 Lemma Qp_mul_le_mono_r p q r : p ≤ q ↔ p * r ≤ q * r.
 Proof. rewrite !(comm_L Qp_mul _ r). apply Qp_mul_le_mono_l. Qed.
@@ -1013,7 +1139,8 @@ Proof. intros. etrans; [by apply Qp_mul_le_mono_l|by apply Qp_mul_le_mono_r]. Qe
 
 Lemma Qp_mul_lt_mono_l p q r : p < q ↔ r * p < r * q.
 Proof.
-  rewrite !Qp_to_Qc_inj_lt. destruct p, q, r; by apply Qcmult_lt_mono_pos_l.
+  assert (0 < Qp_to_Qc r)%Qc by apply Qp_to_Qc_pos.
+  by rewrite !Qp_to_Qc_inj_lt, !Qp_to_Qc_inj_mul, <-Qcmult_lt_mono_pos_l.
 Qed.
 Lemma Qp_mul_lt_mono_r p q r : p < q ↔ p * r < q * r.
 Proof. rewrite !(comm_L Qp_mul _ r). apply Qp_mul_lt_mono_l. Qed.
@@ -1022,8 +1149,9 @@ Proof. intros. etrans; [by apply Qp_mul_lt_mono_l|by apply Qp_mul_lt_mono_r]. Qe
 
 Lemma Qp_lt_add_l p q : p < p + q.
 Proof.
-  destruct p as [p ?], q as [q ?]. apply Qp_to_Qc_inj_lt; simpl.
-  rewrite <- (Qcplus_0_r p) at 1. by rewrite <-Qcplus_lt_mono_l.
+  rewrite !Qp_to_Qc_inj_lt, !Qp_to_Qc_inj_add.
+  rewrite <- (Qcplus_0_r (Qp_to_Qc p)) at 1. rewrite <-Qcplus_lt_mono_l.
+  by apply Qp_to_Qc_pos.
 Qed.
 Lemma Qp_lt_add_r p q : q < p + q.
 Proof. rewrite (comm_L Qp_add). apply Qp_lt_add_l. Qed.
@@ -1043,24 +1171,23 @@ Proof. apply Qp_lt_le_incl, Qp_lt_add_r. Qed.
 
 Lemma Qp_sub_Some p q r : p - q = Some r ↔ p = q + r.
 Proof.
-  destruct p as [p Hp], q as [q Hq], r as [r Hr].
-  unfold Qp_sub, Qp_add; simpl; rewrite <-Qp_to_Qc_inj_iff; simpl. split.
-  - intros; simplify_option_eq. unfold Qcminus.
-    by rewrite (Qcplus_comm p), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
-  - intros ->. unfold Qcminus.
-    rewrite <-Qcplus_assoc, (Qcplus_comm r), Qcplus_assoc.
-    rewrite Qcplus_opp_r, Qcplus_0_l. simplify_option_eq; [|done].
-    f_equal. by apply Qp_to_Qc_inj_iff.
+  rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_add.
+  pose proof (Qp_to_Qc_inj_sub p q) as Hsub.
+  destruct (p - q) as [r'|]; simplify_option_eq.
+  - split.
+    + intros [= ->]. rewrite Hsub. ring.
+    + intros Hp. f_equal. rewrite <-Qp_to_Qc_inj_iff, Hsub, Hp. ring.
+  - split; [done|]. intros Hp. select (¬ _) (fun H => destruct H).
+    rewrite Hp. rewrite <- (Qcplus_0_r (Qp_to_Qc q)) at 1.
+    rewrite <-Qcplus_lt_mono_l. by apply Qp_to_Qc_pos.
 Qed.
 Lemma Qp_lt_sum p q : p < q ↔ ∃ r, q = p + r.
 Proof.
-  destruct p as [p Hp], q as [q Hq]. rewrite Qp_to_Qc_inj_lt; simpl.
-  split.
-  - intros Hlt%Qclt_minus_iff. exists (mk_Qp (q - p) Hlt).
-    apply Qp_to_Qc_inj_iff; simpl. unfold Qcminus.
-    by rewrite (Qcplus_comm q), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
-  - intros [[r ?] ?%Qp_to_Qc_inj_iff]; simplify_eq/=.
-    rewrite <-(Qcplus_0_r p) at 1. by apply Qcplus_lt_mono_l.
+  split; [|intros [r ->]; apply Qp_lt_add_l]. intros Hpq.
+  pose proof (Qp_to_Qc_inj_sub q p) as Hsub.
+  rewrite option_guard_True in Hsub by (by apply Qp_to_Qc_inj_lt).
+  apply fmap_Some in Hsub as [r [? Hr]]. exists r.
+  rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_add, <-Hr. ring.
 Qed.
 
 Lemma Qp_sub_None p q : p - q = None ↔ p ≤ q.
@@ -1232,19 +1359,25 @@ Lemma Qp_min_r_iff q p : q `min` p = p ↔ p ≤ q.
 Proof. rewrite (comm_L Qp_min q). apply Qp_min_l_iff. Qed.
 
 Lemma pos_to_Qp_1 : pos_to_Qp 1 = 1.
-Proof. compute_done. Qed.
+Proof. done. Qed.
 Lemma pos_to_Qp_inj n m : pos_to_Qp n = pos_to_Qp m → n = m.
-Proof. by injection 1. Qed.
+Proof. rewrite <-Qp_to_Qc_inj_iff, !Qp_to_Qc_pos_to_Qp. by injection 1. Qed.
 Lemma pos_to_Qp_inj_iff n m : pos_to_Qp n = pos_to_Qp m ↔ n = m.
 Proof. split; [apply pos_to_Qp_inj|by intros ->]. Qed.
 Lemma pos_to_Qp_inj_le n m : (n ≤ m)%positive ↔ pos_to_Qp n ≤ pos_to_Qp m.
-Proof. rewrite Qp_to_Qc_inj_le; simpl. by rewrite <-Z2Qc_inj_le. Qed.
+Proof. by rewrite Qp_to_Qc_inj_le, !Qp_to_Qc_pos_to_Qp, <-Z2Qc_inj_le. Qed.
 Lemma pos_to_Qp_inj_lt n m : (n < m)%positive ↔ pos_to_Qp n < pos_to_Qp m.
 Proof. by rewrite Pos.lt_nle, Qp_lt_nge, <-pos_to_Qp_inj_le. Qed.
 Lemma pos_to_Qp_add x y : pos_to_Qp x + pos_to_Qp y = pos_to_Qp (x + y).
-Proof. apply Qp_to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_add, Z2Qc_inj_add. Qed.
+Proof.
+  rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_add, !Qp_to_Qc_pos_to_Qp.
+  by rewrite Pos2Z.inj_add, Z2Qc_inj_add.
+Qed.
 Lemma pos_to_Qp_mul x y : pos_to_Qp x * pos_to_Qp y = pos_to_Qp (x * y).
-Proof. apply Qp_to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_mul, Z2Qc_inj_mul. Qed.
+Proof.
+  rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_mul, !Qp_to_Qc_pos_to_Qp.
+  by rewrite Pos2Z.inj_mul, Z2Qc_inj_mul.
+Qed.
 
 Local Close Scope Qp_scope.
 
diff --git a/theories/pmap.v b/theories/pmap.v
index f269f482cec3454211aa5fec2ad30e7a9d51432a..a57840b174ffa5ae2e10ddf6dd4b974cdb400fa5 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -126,24 +126,36 @@ Lemma PNode_lookup {A} o (l r : Pmap_raw A) i :
   PNode' o l r !! i = PNode o l r !! i.
 Proof. by destruct i, o, l, r. Qed.
 
-Lemma Psingleton_wf {A} i (x : A) : Pmap_wf (Psingleton_raw i x).
+Local Lemma Psingleton_wf' {A} i (x : A) : Pmap_wf (Psingleton_raw i x).
 Proof. induction i as [[]|[]|]; simpl; rewrite ?andb_true_r; auto. Qed.
-Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
-  Pmap_wf t → Pmap_wf (Ppartial_alter_raw f i t).
+Local Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
+  SIs_true (Pmap_wf t) → SIs_true (Pmap_wf (Ppartial_alter_raw f i t)).
 Proof.
+  intros Hwf%SIs_true_elim. apply SIs_true_intro. revert Hwf.
   revert i; induction t as [|o l IHl r IHr]; intros i ?; simpl.
-  - destruct (f None); auto using Psingleton_wf.
+  - destruct (f None); auto using Psingleton_wf'.
   - destruct i; simpl; eauto.
 Qed.
-Lemma Pfmap_wf {A B} (f : A → B) t : Pmap_wf t → Pmap_wf (Pfmap_raw f t).
+Local Lemma Pfmap_wf {A B} (f : A → B) t :
+  SIs_true (Pmap_wf t) → SIs_true (Pmap_wf (Pfmap_raw f t)).
 Proof.
+  intros Hwf%SIs_true_elim. apply SIs_true_intro. revert Hwf.
   induction t as [|[x|] [] ? [] ?]; simpl in *; rewrite ?andb_True; intuition.
 Qed.
-Lemma Pomap_wf {A B} (f : A → option B) t : Pmap_wf t → Pmap_wf (Pomap_raw f t).
+Local Lemma Pomap_wf' {A B} (f : A → option B) t :
+  Pmap_wf t → Pmap_wf (Pomap_raw f t).
 Proof. induction t; simpl; eauto. Qed.
-Lemma Pmerge_wf {A B C} (f : option A → option B → option C) t1 t2 :
-  Pmap_wf t1 → Pmap_wf t2 → Pmap_wf (Pmerge_raw f t1 t2).
-Proof. revert t2. induction t1; intros []; simpl; eauto using Pomap_wf. Qed.
+Local Lemma Pomap_wf {A B} (f : A → option B) t :
+  SIs_true (Pmap_wf t) → SIs_true (Pmap_wf (Pomap_raw f t)).
+Proof. intros. by apply SIs_true_intro, Pomap_wf', SIs_true_elim. Qed.
+Local Lemma Pmerge_wf {A B C} (f : option A → option B → option C) t1 t2 :
+  SIs_true (Pmap_wf t1) → SIs_true (Pmap_wf t2) →
+  SIs_true (Pmap_wf (Pmerge_raw f t1 t2)).
+Proof.
+  intros Hwf1%SIs_true_elim Hwf2%SIs_true_elim.
+  apply SIs_true_intro. revert Hwf1 Hwf2.
+  revert t2. induction t1; intros []; simpl; eauto using Pomap_wf'.
+Qed.
 
 Lemma Plookup_empty {A} i : (∅ : Pmap_raw A) !! i = None.
 Proof. by destruct i. Qed.
@@ -254,38 +266,42 @@ Proof.
 Qed.
 
 (** Packed version and instance of the finite map type class *)
-Inductive Pmap (A : Type) : Type :=
-  PMap { pmap_car : Pmap_raw A; pmap_prf : Pmap_wf pmap_car }.
+Record Pmap (A : Type) : Type :=
+  PMap { pmap_car : Pmap_raw A; pmap_prf : SIs_true (Pmap_wf pmap_car) }.
 Global Arguments PMap {_} _ _ : assert.
 Global Arguments pmap_car {_} _ : assert.
 Global Arguments pmap_prf {_} _ : assert.
+
 Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2 ↔ pmap_car m1 = pmap_car m2.
 Proof.
   split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
-  simplify_eq/=; f_equal; apply proof_irrel.
+  simplify_eq/=; f_equal.
 Qed.
 Global Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
   match Pmap_raw_eq_dec (pmap_car m1) (pmap_car m2) with
   | left H => left (proj2 (Pmap_eq m1 m2) H)
   | right H => right (H ∘ proj1 (Pmap_eq m1 m2))
   end.
-Global Instance Pempty {A} : Empty (Pmap A) := PMap ∅ I.
+
+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 m,
-  let (t,Ht) := m in PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
-Global Instance Pfmap : FMap Pmap := λ A B f m,
-  let (t,Ht) := m in PMap (f <$> t) (Pfmap_wf f _ Ht).
-Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
-  let (t,Ht) := m in Pto_list_raw 1 t [].
-Global Instance Pomap : OMap Pmap := λ A B f m,
-  let (t,Ht) := m in PMap (omap f t) (Pomap_wf f _ Ht).
-Global Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
-  let (t1,Ht1) := m1 in let (t2,Ht2) := m2 in PMap _ (Pmerge_wf f _ _ Ht1 Ht2).
+Global Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) :=
+  λ f i '(PMap t Ht),
+    PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
+Global Instance Pfmap : FMap Pmap := λ A B f '(PMap t Ht),
+  PMap (f <$> t) (Pfmap_wf f _ Ht).
+Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ '(PMap t Ht),
+  Pto_list_raw 1 t [].
+Global Instance Pomap : OMap Pmap := λ A B f '(PMap t Ht),
+  PMap (omap f t) (Pomap_wf f _ Ht).
+Global Instance Pmerge : Merge Pmap := λ A B C f '(PMap t1 Ht1) '(PMap t2 Ht2),
+  PMap _ (Pmerge_wf f _ _ Ht1 Ht2).
 
 Global Instance Pmap_finmap : FinMap positive Pmap.
 Proof.
-  split.
-  - by intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq.
+ split.
+  - intros ? [t1 ?] [t2 ?] ?.
+    apply Pmap_eq, Pmap_wf_eq; auto using SIs_true_elim.
   - by intros ? [].
   - intros ?? [??] ?. by apply Plookup_alter.
   - intros ?? [??] ??. by apply Plookup_alter_ne.