diff --git a/theories/assoc.v b/theories/assoc.v
index 37dc2f90c521ec814e13de5f571acfc0fbaec9b5..370b447b124c318f4d23895d7906506473f9d8ed 100644
--- a/theories/assoc.v
+++ b/theories/assoc.v
@@ -271,7 +271,7 @@ End assoc.
 
 (** * Finite sets *)
 (** We construct finite sets using the above implementation of maps. *)
-Notation assoc_set K := (mapset (assoc K)).
+Notation assoc_set K := (mapset (assoc K unit)).
 Instance assoc_map_dom `{Lexico K, !TrichotomyT (@lexico K _),
   !StrictOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
 Instance assoc_map_dom_spec `{Lexico K} `{!TrichotomyT (@lexico K _)}
diff --git a/theories/base.v b/theories/base.v
index d2b78fb670322c1af2ec66a373a1f0d5f60b364b..cf7f74c5228ec35d4922c4c3e895882e929a3d01 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -32,6 +32,10 @@ Notation "'False'" := False : type_scope.
 
 Notation curry := prod_curry.
 Notation uncurry := prod_uncurry.
+Definition curry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=
+  let '(a,b,c) := p in f a b c.
+Definition curry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D) : E :=
+  let '(a,b,c,d) := p in f a b c d.
 
 (** Throughout this development we use [C_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
@@ -376,45 +380,24 @@ Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B →
 
 (** ** Monadic operations *)
 (** We define operational type classes for the monadic operations bind, join 
-and fmap. These type classes are defined in a non-standard way by taking the
-function as a parameter of the class. For example, we define
-<<
-  Class FMapD := fmap: ∀ {A B}, (A → B) → M A → M B.
->>
-instead of
-<<
-  Class FMap {A B} (f : A → B) := fmap: M A → M B.
->>
-This approach allows us to define [fmap] on lists such that [simpl] unfolds it
-in the appropriate way, and so that it can be used for mutual recursion
-(the mapped function [f] is not part of the fixpoint) as well. This is a hack,
-and should be replaced by something more appropriate in future versions. *)
-
-(** We use these type classes merely for convenient overloading of notations and
-do not formalize any theory on monads (we do not even define a class with the
-monad laws). *)
+and fmap. We use these type classes merely for convenient overloading of
+notations and do not formalize any theory on monads (we do not even define a
+class with the monad laws). *)
 Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
 Instance: Params (@mret) 3.
 Arguments mret {_ _ _} _.
-
-Class MBindD (M : Type → Type) {A B} (f : A → M B) := mbind: M A → M B.
-Notation MBind M := (∀ {A B} (f : A → M B), MBindD M f)%type.
+Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
+Arguments mbind {_ _ _ _} _ !_ /.
 Instance: Params (@mbind) 5.
-Arguments mbind {_ _ _} _ {_} !_ /.
-
 Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A.
 Instance: Params (@mjoin) 3.
 Arguments mjoin {_ _ _} !_ /.
-
-Class FMapD (M : Type → Type) {A B} (f : A → B) := fmap: M A → M B.
-Notation FMap M := (∀ {A B} (f : A → B), FMapD M f)%type.
+Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
 Instance: Params (@fmap) 6.
-Arguments fmap {_ _ _} _ {_} !_ /.
-
-Class OMapD (M : Type → Type) {A B} (f : A → option B) := omap: M A → M B.
-Notation OMap M := (∀ {A B} (f : A → option B), OMapD M f)%type.
+Arguments fmap {_ _ _ _} _ !_ /.
+Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B.
 Instance: Params (@omap) 6.
-Arguments omap {_ _ _} _ {_} !_ /.
+Arguments omap {_ _ _ _} _ !_ /.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
 Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : C_scope.
@@ -430,6 +413,9 @@ Notation "'( x1 , x2 ) ← y ; z" :=
 Notation "'( x1 , x2 , x3 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3) := x in z))
   (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+Notation "'( x1 , x2 , x3  , x4 ) ← y ; z" :=
+  (y ≫= (λ x : _, let ' (x1,x2,x3,x4) := x in z))
+  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
 
 Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
@@ -468,10 +454,9 @@ Arguments delete _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
-Class AlterD (K A M : Type) (f : A → A) := alter: K → M → M.
-Notation Alter K A M := (∀ (f : A → A), AlterD K A M f)%type.
+Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
 Instance: Params (@alter) 5.
-Arguments alter {_ _ _} _ {_} !_ !_ / : simpl nomatch.
+Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value at key [k] or [None]
diff --git a/theories/countable.v b/theories/countable.v
index 73b5ff72f4c4d2984bbff1c5fb406252cb2c0a40..bd62102163d34420bf0bbaa8b71188b6313cd4bc 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -165,7 +165,7 @@ Program Instance prod_countable `{Countable A} `{Countable B} :
 Next Obligation.
   intros ?????? [x y]; simpl.
   rewrite prod_decode_encode_fst, prod_decode_encode_snd.
-  simpl. by rewrite !decode_encode.
+  csimpl. by rewrite !decode_encode.
 Qed.
 
 Fixpoint list_encode_ (l : list positive) : positive :=
@@ -188,7 +188,7 @@ Lemma list_decode_encode l : list_decode (list_encode l) = Some l.
 Proof.
   cut (list_decode_ (length l) (list_encode_ l) = Some l).
   { intros help. unfold list_decode, list_encode.
-    rewrite prod_decode_encode_fst, prod_decode_encode_snd; simpl.
+    rewrite prod_decode_encode_fst, prod_decode_encode_snd; csimpl.
     by rewrite Nat2Pos.id by done; simpl. }
   induction l; simpl; auto.
   by rewrite prod_decode_encode_fst, prod_decode_encode_snd;
@@ -227,5 +227,5 @@ Program Instance nat_countable : Countable nat := {|
   decode p := N.to_nat <$> decode p
 |}.
 Next Obligation.
-  intros x. rewrite decode_encode; simpl. by rewrite Nat2N.id.
+  intros x. rewrite decode_encode; csimpl. by rewrite Nat2N.id.
 Qed.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 66ce3e083eb889159e75b3b478bd8316adcfe97d..a8a59ee8694607d376b13c7141b326bc1fe660e8 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -205,9 +205,9 @@ Lemma alter_ext {A} (f g : A → A) (m : M A) i :
   (∀ x, m !! i = Some x → f x = g x) → alter f i m = alter g i m.
 Proof. intro. apply partial_alter_ext. intros [x|] ?; f_equal'; auto. Qed.
 Lemma lookup_alter {A} (f : A → A) m i : alter f i m !! i = f <$> m !! i.
-Proof. apply lookup_partial_alter. Qed.
+Proof. unfold alter. apply lookup_partial_alter. Qed.
 Lemma lookup_alter_ne {A} (f : A → A) m i j : i ≠ j → alter f i m !! j = m !! j.
-Proof. apply lookup_partial_alter_ne. Qed.
+Proof. unfold alter. apply lookup_partial_alter_ne. Qed.
 Lemma alter_compose {A} (f g : A → A) (m : M A) i:
   alter (f ∘ g) i m = alter f i (alter g i m).
 Proof.
@@ -375,6 +375,13 @@ Proof.
   * eauto using insert_delete_subset.
   * by rewrite lookup_delete.
 Qed.
+Lemma fmap_insert {A B} (f : A → B) (m : M A) i x :
+  f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
+Proof.
+  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
+  * by rewrite lookup_fmap, !lookup_insert.
+  * by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
+Qed.
 
 (** ** Properties of the singleton maps *)
 Lemma lookup_singleton_Some {A} i j (x y : A) :
@@ -430,7 +437,7 @@ Proof. eauto using NoDup_fmap_fst, map_to_list_unique, NoDup_map_to_list. Qed.
 Lemma elem_of_map_of_list_1 {A} (l : list (K * A)) i x :
   NoDup (fst <$> l) → (i,x) ∈ l → map_of_list l !! i = Some x.
 Proof.
-  induction l as [|[j y] l IH]; simpl; [by rewrite elem_of_nil|].
+  induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|].
   rewrite NoDup_cons, elem_of_cons, elem_of_list_fmap.
   intros [Hl ?] [?|?]; simplify_equality; [by rewrite lookup_insert|].
   destruct (decide (i = j)) as [->|]; [|rewrite lookup_insert_ne; auto].
@@ -455,7 +462,7 @@ Qed.
 Lemma not_elem_of_map_of_list_2 {A} (l : list (K * A)) i :
   map_of_list l !! i = None → i ∉ fst <$> l.
 Proof.
-  induction l as [|[j y] l IH]; simpl; [rewrite elem_of_nil; tauto|].
+  induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|].
   rewrite elem_of_cons. destruct (decide (i = j)); simplify_equality.
   * by rewrite lookup_insert.
   * by rewrite lookup_insert_ne; intuition.
@@ -499,7 +506,7 @@ Qed.
 Lemma map_to_list_insert {A} (m : M A) i x :
   m !! i = None → map_to_list (<[i:=x]>m) ≡ₚ (i,x) :: map_to_list m.
 Proof.
-  intros. apply map_of_list_inj; simpl.
+  intros. apply map_of_list_inj; csimpl.
   * apply NoDup_fst_map_to_list.
   * constructor; auto using NoDup_fst_map_to_list.
     rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
@@ -521,7 +528,7 @@ Proof.
   intros Hperm. apply map_to_list_inj.
   assert (NoDup (fst <$> (i, x) :: l)) as Hnodup.
   { rewrite <-Hperm. auto using NoDup_fst_map_to_list. }
-  simpl in Hnodup. rewrite NoDup_cons in Hnodup. destruct Hnodup.
+  csimpl in *. rewrite NoDup_cons in Hnodup. destruct Hnodup.
   rewrite Hperm, map_to_list_insert, map_to_of_list;
     auto using not_elem_of_map_of_list_1.
 Qed.
@@ -1374,7 +1381,7 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
   | H : ∅ = {[?i,?x]} |- _ => by destruct (map_non_empty_singleton i x)
   end.
 Tactic Notation "simplify_map_equality'" "by" tactic3(tac) :=
-  repeat (progress simpl in * || simplify_map_equality by tac).
+  repeat (progress csimpl in * || simplify_map_equality by tac).
 Tactic Notation "simplify_map_equality" :=
   simplify_map_equality by eauto with simpl_map map_disjoint.
 Tactic Notation "simplify_map_equality'" :=
diff --git a/theories/finite.v b/theories/finite.v
index 2dc8b648cec2ac81f472da46d546818773cf8bde..48056ab8cec38a22f9b0599c9448e8c511cd199b 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -56,7 +56,7 @@ Proof.
   destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
   intros Hx. destruct (list_find_elem_of P xs x) as [i Hi]; auto.
   rewrite Hi. destruct (list_find_Some P xs i) as (y&?&?); subst; auto.
-  exists y. simpl. by rewrite !Nat2Pos.id by done.
+  exists y. csimpl. by rewrite !Nat2Pos.id by done.
 Qed.
 
 Lemma card_0_inv P `{finA: Finite A} : card A = 0 → A → P.
diff --git a/theories/hashset.v b/theories/hashset.v
index 509fd914b7255dabaa55b27c05b6eb5669d45f9a..2cb6359f72607b7e681a99451fc387a16a03ddbf 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -3,7 +3,7 @@
 (** This file implements finite set using hash maps. Hash sets are represented
 using radix-2 search trees. Each hash bucket is thus indexed using an binary
 integer of type [Z], and contains an unordered list without duplicates. *)
-Require Export fin_maps.
+Require Export fin_maps listset.
 Require Import zmap.
 
 Record hashset {A} (hash : A → Z) := Hashset {
@@ -15,7 +15,7 @@ Arguments Hashset {_ _} _ _.
 Arguments hashset_car {_ _} _.
 
 Section hashset.
-Context {A : Type} {hash : A → Z} `{∀ x y : A, Decision (x = y)}.
+Context `{∀ x y : A, Decision (x = y)} (hash : A → Z).
 
 Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l,
   hashset_car m !! hash x = Some l ∧ x ∈ l.
@@ -106,7 +106,7 @@ Proof.
   * unfold elements, hashset_elems. intros [m Hm]; simpl.
     rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
     induction Hm as [|[n l] m' [??]];
-      simpl; inversion_clear 1 as [|?? Hn]; [constructor|].
+      csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
     apply NoDup_app; split_ands; eauto.
     setoid_rewrite elem_of_list_bind; intros x ? ([n' l']&?&?); simpl in *.
     assert (hash x = n ∧ hash x = n') as [??]; subst.
@@ -115,6 +115,25 @@ Proof.
       rewrite Forall_forall in Hm. eapply (Hm (_,_)); eauto. }
     destruct Hn; rewrite elem_of_list_fmap; exists (hash x, l'); eauto.
 Qed.
+
+Definition remove_dups_fast (l : list A) : list A :=
+  elements (foldr (λ x, ({[ x ]} ∪)) ∅ l : hashset hash).
+Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l.
+Proof.
+  unfold remove_dups_fast. rewrite elem_of_elements. split.
+  * revert x. induction l as [|y l IH]; intros x; simpl.
+    { by rewrite elem_of_empty. }
+    rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto.
+  * induction 1; esolve_elem_of.
+Qed.
+Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
+Proof. unfold remove_dups_fast. apply NoDup_elements. Qed.
+Definition listset_normalize (X : listset A) : listset A :=
+  let (l) := X in Listset (remove_dups_fast l).
+Lemma listset_normalize_correct X : listset_normalize X ≡ X.
+Proof.
+  destruct X as [l]. apply elem_of_equiv; intro; apply elem_of_remove_dups_fast.
+Qed.
 End hashset.
 
 (** These instances are declared using [Hint Extern] to avoid too
diff --git a/theories/list.v b/theories/list.v
index 4ccbef4c7f4484938b193f060283ec9ab61aed60..dafe8d95737eb257af26ee1bb3d0923e2711f3d0 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -45,11 +45,11 @@ Instance list_lookup {A} : Lookup nat A (list A) :=
 
 (** The operation [alter f i l] applies the function [f] to the [i]th element
 of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
-Instance list_alter {A} (f : A → A) : AlterD nat A (list A) f :=
-  fix go i l {struct l} := let _ : AlterD _ _ _ f := @go in
+Instance list_alter {A} : Alter nat A (list A) := λ f,
+  fix go i l {struct l} :=
   match l with
   | [] => []
-  | x :: l => match i with 0 => f x :: l | S i => x :: alter f i l end
+  | x :: l => match i with 0 => f x :: l | S i => x :: go i l end
   end.
 
 (** The operation [<[i:=x]> l] overwrites the element at position [i] with the
@@ -139,12 +139,10 @@ Definition foldl {A B} (f : A → B → A) : A → list B → A :=
 
 (** The monadic operations. *)
 Instance list_ret: MRet list := λ A x, x :: @nil A.
-Instance list_fmap {A B} (f : A → B) : FMapD list f :=
-  fix go (l : list A) :=
-  match l with [] => [] | x :: l => f x :: @fmap _ _ _ f go l end.
-Instance list_bind {A B} (f : A → list B) : MBindD list f :=
-  fix go (l : list A) :=
-  match l with [] => [] | x :: l => f x ++ @mbind _ _ _ f go l end.
+Instance list_fmap : FMap list := λ A B f,
+  fix go (l : list A) := match l with [] => [] | x :: l => f x :: go l end.
+Instance list_bind : MBind list := λ A B f,
+  fix go (l : list A) := match l with [] => [] | x :: l => f x ++ go l end.
 Instance list_join: MJoin list :=
   fix go A (ls : list (list A)) : list A :=
   match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
@@ -192,6 +190,8 @@ Definition suffix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
 Definition prefix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k.
 Infix "`suffix_of`" := suffix_of (at level 70) : C_scope.
 Infix "`prefix_of`" := prefix_of (at level 70) : C_scope.
+Hint Extern 0 (?x `prefix_of` ?y) => reflexivity.
+Hint Extern 0 (?x `suffix_of` ?y) => reflexivity.
 
 Section prefix_suffix_ops.
   Context `{∀ x y : A, Decision (x = y)}.
@@ -219,6 +219,7 @@ Inductive sublist {A} : relation (list A) :=
   | sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
   | sublist_cons x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
 Infix "`sublist`" := sublist (at level 70) : C_scope.
+Hint Extern 0 (?x `sublist` ?y) => reflexivity.
 
 (** A list [l2] contains a list [l1] if [l2] is obtained by removing elements
 from [l1] while possiblity changing the order. *)
@@ -229,6 +230,7 @@ Inductive contains {A} : relation (list A) :=
   | contains_cons x l1 l2 : contains l1 l2 → contains l1 (x :: l2)
   | contains_trans l1 l2 l3 : contains l1 l2 → contains l2 l3 → contains l1 l3.
 Infix "`contains`" := contains (at level 70) : C_scope.
+Hint Extern 0 (?x `contains` ?y) => reflexivity.
 
 Section contains_dec_help.
   Context {A} {dec : ∀ x y : A, Decision (x = y)}.
@@ -439,7 +441,7 @@ Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
 Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
 Lemma list_lookup_alter_ne f l i j : i ≠ j → alter f i l !! j = l !! j.
 Proof.
-  revert i j. induction l; [done|]. intros [] [] ?; simpl; auto with congruence.
+  revert i j. induction l; [done|]. intros [][] ?; csimpl; auto with congruence.
 Qed.
 Lemma list_lookup_insert l i x : i < length l → <[i:=x]>l !! i = Some x.
 Proof. revert i. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
@@ -2390,7 +2392,7 @@ Section fmap.
   Proof. by induction l; f_equal'. Qed.
   Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
   Proof.
-    induction l as [|?? IH]; simpl; by rewrite ?reverse_cons, ?fmap_app, ?IH.
+    induction l as [|?? IH]; csimpl; by rewrite ?reverse_cons, ?fmap_app, ?IH.
   Qed.
   Lemma fmap_last l : last (f <$> l) = f <$> last l.
   Proof. induction l as [|? []]; simpl; auto. Qed.
@@ -2419,7 +2421,7 @@ Section fmap.
     Forall (λ x, f (g x) = h (f x)) l → f <$> alter g i l = alter h i (f <$> l).
   Proof. intros Hl. revert i. by induction Hl; intros [|i]; f_equal'. Qed.
   Lemma elem_of_list_fmap_1 l x : x ∈ l → f x ∈ f <$> l.
-  Proof. induction 1; simpl; rewrite elem_of_cons; intuition. Qed.
+  Proof. induction 1; csimpl; rewrite elem_of_cons; intuition. Qed.
   Lemma elem_of_list_fmap_1_alt l x y : x ∈ l → y = f x → y ∈ f <$> l.
   Proof. intros. subst. by apply elem_of_list_fmap_1. Qed.
   Lemma elem_of_list_fmap_2 l x : x ∈ f <$> l → ∃ y, x = f y ∧ y ∈ l.
@@ -2478,7 +2480,7 @@ Section fmap.
   Proof. revert l2; induction l1; intros [|??]; inversion_clear 1; auto. Qed.
   Lemma Forall2_fmap_2 {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
     Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2 → Forall2 P (f <$> l1) (g <$> l2).
-  Proof. induction 1; simpl; auto. Qed.
+  Proof. induction 1; csimpl; auto. Qed.
   Lemma Forall2_fmap {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
     Forall2 P (f <$> l1) (g <$> l2) ↔ Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
   Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
@@ -2492,7 +2494,7 @@ Proof. auto using list_alter_fmap. Qed.
 Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
   (∀ x y1 y2, (x,y1) ∈ l → (x,y2) ∈ l → y1 = y2) → NoDup l → NoDup (fst <$> l).
 Proof.
-  intros Hunique. induction 1 as [|[x1 y1] l Hin Hnodup IH]; simpl; constructor.
+  intros Hunique. induction 1 as [|[x1 y1] l Hin Hnodup IH]; csimpl; constructor.
   * rewrite elem_of_list_fmap.
     intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
     rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
@@ -2511,12 +2513,11 @@ Section bind.
   Global Instance bind_sublist: Proper (sublist ==> sublist) (mbind f).
   Proof.
     induction 1; simpl; auto;
-      [done|by apply sublist_app|by apply sublist_inserts_l].
+      [by apply sublist_app|by apply sublist_inserts_l].
   Qed.
   Global Instance bind_contains: Proper (contains ==> contains) (mbind f).
   Proof.
-    induction 1; simpl; auto.
-    * done.
+    induction 1; csimpl; auto.
     * by apply contains_app.
     * by rewrite !(associative_L (++)), (commutative (++) (f _)).
     * by apply contains_inserts_l.
@@ -2524,7 +2525,7 @@ Section bind.
   Qed.
   Global Instance bind_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (mbind f).
   Proof.
-    induction 1; simpl; auto.
+    induction 1; csimpl; auto.
     * by f_equiv.
     * by rewrite !(associative_L (++)), (commutative (++) (f _)).
     * etransitivity; eauto.
@@ -2532,30 +2533,30 @@ Section bind.
   Lemma bind_cons x l : (x :: l) ≫= f = f x ++ l ≫= f.
   Proof. done. Qed.
   Lemma bind_singleton x : [x] ≫= f = f x.
-  Proof. simpl. by rewrite (right_id_L _ (++)). Qed.
+  Proof. csimpl. by rewrite (right_id_L _ (++)). Qed.
   Lemma bind_app l1 l2 : (l1 ++ l2) ≫= f = (l1 ≫= f) ++ (l2 ≫= f).
-  Proof. by induction l1; simpl; rewrite <-?(associative_L (++)); f_equal. Qed.
+  Proof. by induction l1; csimpl; rewrite <-?(associative_L (++)); f_equal. Qed.
   Lemma elem_of_list_bind (x : B) (l : list A) :
     x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
   Proof.
     split.
-    * induction l as [|y l IH]; simpl; [inversion 1|].
+    * induction l as [|y l IH]; csimpl; [inversion 1|].
       rewrite elem_of_app. intros [?|?].
       + exists y. split; [done | by left].
       + destruct IH as [z [??]]. done. exists z. split; [done | by right].
-    * intros [y [Hx Hy]]. induction Hy; simpl; rewrite elem_of_app; intuition.
+    * intros [y [Hx Hy]]. induction Hy; csimpl; rewrite elem_of_app; intuition.
   Qed.
   Lemma Forall_bind (P : B → Prop) l :
     Forall P (l ≫= f) ↔ Forall (Forall P ∘ f) l.
   Proof.
     split.
-    * induction l; simpl; rewrite ?Forall_app; constructor; simpl; intuition.
-    * induction 1; simpl; rewrite ?Forall_app; auto.
+    * induction l; csimpl; rewrite ?Forall_app; constructor; csimpl; intuition.
+    * induction 1; csimpl; rewrite ?Forall_app; auto.
   Qed.
   Lemma Forall2_bind {C D} (g : C → list D) (P : B → D → Prop) l1 l2 :
     Forall2 (λ x1 x2, Forall2 P (f x1) (g x2)) l1 l2 →
     Forall2 P (l1 ≫= f) (l2 ≫= g).
-  Proof. induction 1; simpl; auto using Forall2_app. Qed.
+  Proof. induction 1; csimpl; auto using Forall2_app. Qed.
 End bind.
 
 Section ret_join.
@@ -2676,7 +2677,7 @@ Section permutations.
   Lemma permutations_swap x y l : y :: x :: l ∈ permutations (x :: y :: l).
   Proof.
     simpl. apply elem_of_list_bind. exists (y :: l). split; simpl.
-    * destruct l; simpl; rewrite !elem_of_cons; auto.
+    * destruct l; csimpl; rewrite !elem_of_cons; auto.
     * apply elem_of_list_bind. simpl.
       eauto using interleave_cons, permutations_refl.
   Qed.
@@ -2694,12 +2695,12 @@ Section permutations.
     intros Hl1 [? | [l2' [??]]]; simplify_equality'.
     * rewrite !elem_of_cons, elem_of_list_fmap in Hl1.
       destruct Hl1 as [? | [? | [l4 [??]]]]; subst.
-      + exists (x1 :: y :: l3). simpl. rewrite !elem_of_cons. tauto.
-      + exists (x1 :: y :: l3). simpl. rewrite !elem_of_cons. tauto.
+      + exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
+      + exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
       + exists l4. simpl. rewrite elem_of_cons. auto using interleave_cons.
     * rewrite elem_of_cons, elem_of_list_fmap in Hl1.
       destruct Hl1 as [? | [l1' [??]]]; subst.
-      + exists (x1 :: y :: l3). simpl.
+      + exists (x1 :: y :: l3). csimpl.
         rewrite !elem_of_cons, !elem_of_list_fmap.
         split; [| by auto]. right. right. exists (y :: l2').
         rewrite elem_of_list_fmap. naive_solver.
@@ -3006,7 +3007,7 @@ Section eval.
 
   Lemma eval_alt t : eval E t = to_list t ≫= from_option [] ∘ (E !!).
   Proof.
-    induction t; simpl.
+    induction t; csimpl.
     * done.
     * by rewrite (right_id_L [] (++)).
     * rewrite bind_app. by f_equal.
diff --git a/theories/map.v b/theories/map.v
deleted file mode 100644
index 89350a68b461588e2a9c75a4131ea31abedd5e1c..0000000000000000000000000000000000000000
--- a/theories/map.v
+++ /dev/null
@@ -1,144 +0,0 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
-(* This file is distributed under the terms of the BSD license. *)
-Require Export separation.
-Require Import refinements.
-
-Record map (A : Set) := Map { map_car : indexmap (list A) }.
-Arguments Map {_} _.
-Arguments map_car {_} _.
-Add Printing Constructor map.
-Instance: Injective (=) (=) (@Map A).
-Proof. by injection 1. Qed.
-
-Instance map_ops {A : Set} `{SeparationOps A} : SeparationOps (map A) := {
-  sep_empty := Map ∅;
-  sep_union m1 m2 :=
-    let (m1) := m1 in let (m2) := m2 in
-    Map (union_with (λ xs1 xs2, Some (xs1 ∪* xs2)) m1 m2);
-  sep_difference m1 m2 :=
-    let (m1) := m1 in let (m2) := m2 in
-    Map (difference_with (λ xs1 xs2,
-      let xs' := xs1 ∖* xs2 in guard (¬Forall (∅ =) xs'); Some xs'
-    ) m1 m2);
-  sep_half m := let (m) := m in Map (½* <$> m);
-  sep_valid m :=
-    let (m) := m in map_Forall (λ _ xs, Forall sep_valid xs ∧ ¬Forall (∅ =) xs) m;
-  sep_disjoint m1 m2 :=
-    let (m1) := m1 in let (m2) := m2 in map_Forall2
-      (λ xs1 xs2, xs1 ⊥* xs2 ∧ ¬Forall (∅ =) xs1 ∧ ¬Forall (∅ =) xs2) 
-      (λ xs1, Forall sep_valid xs1 ∧ ¬Forall (∅ =) xs1)
-      (λ xs2, Forall sep_valid xs2 ∧ ¬Forall (∅ =) xs2) m1 m2;
-  sep_splittable m :=
-    let (m) := m in
-    map_Forall (λ _ xs,
-      Forall sep_valid xs ∧ ¬Forall (∅ =) xs ∧ Forall sep_splittable xs) m;
-  sep_subseteq m1 m2 :=
-    let (m1) := m1 in let (m2) := m2 in map_Forall2
-      (λ xs1 w2, xs1 ⊆* w2 ∧ ¬Forall (∅ =) xs1)
-      (λ xs1, False)
-      (λ xs2, Forall sep_valid xs2 ∧ ¬Forall (∅ =) xs2) m1 m2;
-  sep_unmapped m := map_car m = ∅;
-  sep_unshared m := False
-}.
-Proof.
-  * intros []; apply _.
-  * intros [] []; apply _.
-  * intros [] []; apply _.
-  * solve_decision.
-  * intros []; apply _.
-Defined.
-
-Instance map_sep {A : Set} `{Separation A} : Separation (map A).
-Proof.
-  split.
-  * destruct (sep_inhabited A) as (x&?&?).
-    eexists (Map {[fresh ∅, [x]]}).
-    split; [|by intro]. intros o w ?; simplify_map_equality'. split.
-    + by rewrite Forall_singleton.
-    + by inversion_clear 1; decompose_Forall_hyps'.
-  * sep_unfold; intros [m1] [m2] Hm o w; specialize (Hm o); simpl in *.
-    intros Hx. rewrite Hx in Hm.
-    destruct (m2 !! o); intuition eauto using seps_disjoint_valid_l.
-  * sep_unfold; intros [m1] [m2] Hm o w; specialize (Hm o); simpl in *.
-    rewrite lookup_union_with. intros. destruct (m1 !! o), (m2 !! o);
-    simplify_equality'; intuition eauto using seps_union_valid, seps_positive_l.
-  * sep_unfold. intros [m] Hm o; specialize (Hm o); simplify_map_equality'.
-    destruct (m !! o); eauto.
-  * sep_unfold; intros [m] ?; f_equal'. by rewrite (left_id_L ∅ _).
-  * sep_unfold. intros [m1] [m2] Hm o; specialize (Hm o); simpl in *.
-    destruct (m1 !! o), (m2 !! o); intuition.
-  * sep_unfold; intros [m1] [m2] Hm; f_equal'. apply union_with_commutative.
-    intros o w1 w2 ??; specialize (Hm o); simplify_option_equality.
-    f_equal; intuition auto using seps_commutative.
-  * sep_unfold; intros [m1] [m2] [m3] Hm Hm' o; specialize (Hm o);
-      specialize (Hm' o); simpl in *; rewrite lookup_union_with in Hm'.
-    destruct (m1 !! o) eqn:?, (m2 !! o), (m3 !! o); simplify_equality';
-      intuition eauto using seps_disjoint_valid_l, seps_disjoint_ll.
-  * sep_unfold; intros [m1] [m2] [m3] Hm Hm' o; specialize (Hm o);
-      specialize (Hm' o); simpl in *; rewrite lookup_union_with in Hm' |- *.
-    destruct (m1 !! o) eqn:?, (m2 !! o), (m3 !! o); simplify_equality';
-      intuition eauto using seps_disjoint_valid_l, seps_disjoint_move_l,
-      seps_union_valid, seps_positive_l, seps_disjoint_lr.
-  * sep_unfold; intros [m1] [m2] [m3] Hm Hm'; f_equal'.
-    apply map_eq; intros o; specialize (Hm o); specialize (Hm' o); simpl in *;
-      rewrite !lookup_union_with; rewrite lookup_union_with in Hm'.
-    destruct (m1 !! o) eqn:?, (m2 !! o), (m3 !! o); simplify_equality'; eauto.
-    f_equal; intuition auto using seps_associative.
-  * sep_unfold; intros [m1] [m2] _; rewrite !(injective_iff Map); intros Hm.
-    apply map_eq; intros o. rewrite lookup_empty.
-    apply (f_equal (!! o)) in Hm; rewrite lookup_union_with, lookup_empty in Hm.
-    by destruct (m1 !! o), (m2 !! o); simplify_equality'.
-  * sep_unfold; intros [m1] [m2] [m3] Hm Hm'; rewrite !(injective_iff Map);
-      intros Hm''; apply map_eq; intros o.
-    specialize (Hm o); specialize (Hm' o);
-      apply (f_equal (!! o)) in Hm''; rewrite !lookup_union_with in Hm''.
-    destruct (m1 !! o) eqn:?, (m2 !! o), (m3 !! o); simplify_equality';
-      f_equal; naive_solver eauto using seps_cancel_l,
-      seps_cancel_empty_l, seps_cancel_empty_r.
-  * sep_unfold; intros [m1] [m2] Hm o; specialize (Hm o).
-    rewrite lookup_union_with. destruct (m1 !! o), (m2 !! o); simpl;
-      intuition auto using seps_union_subseteq_l, seps_reflexive.
-  * sep_unfold; intros [m1] [m2] Hm o; specialize (Hm o).
-    rewrite lookup_difference_with; destruct (m1 !! o), (m2 !! o);
-      simplify_option_equality;
-      intuition eauto using seps_disjoint_difference, seps_disjoint_valid_l.
-  * sep_unfold; intros [m1] [m2] Hm; f_equal; apply map_eq; intros o;
-      specialize (Hm o); rewrite lookup_union_with, lookup_difference_with.
-    destruct (m1 !! o), (m2 !! o); simplify_option_equality; f_equal;
-      intuition eauto using seps_union_difference, seps_difference_empty_rev.
-  * sep_unfold; intros [m] Hm o w; specialize (Hm o).
-    rewrite lookup_union_with; intros; destruct (m !! o); simplify_equality'.
-    intuition eauto using seps_union_valid,
-      seps_splittable_union, seps_positive_l.
-  * sep_unfold; intros [m1] [m2] Hm Hm' o w ?; specialize (Hm o);
-      specialize (Hm' o); simplify_option_equality.
-    destruct (m2 !! o); naive_solver eauto using seps_disjoint_difference,
-      seps_disjoint_valid_l, seps_splittable_weaken.
-  * sep_unfold; intros [m] Hm o; specialize (Hm o); rewrite lookup_fmap.
-    destruct (m !! o); try naive_solver
-      auto using seps_half_empty_rev, seps_disjoint_half.
-  * sep_unfold; intros [m] Hm; f_equal; apply map_eq; intros o;
-      specialize (Hm o); rewrite lookup_union_with, lookup_fmap.
-    destruct (m !! o); f_equal'; naive_solver auto using seps_union_half.
-  * sep_unfold; intros [m1] [m2] Hm Hm'; f_equal; apply map_eq; intros o;
-      rewrite lookup_fmap, !lookup_union_with, !lookup_fmap;
-      specialize (Hm o); specialize (Hm' o); rewrite lookup_union_with in Hm'.
-    destruct (m1 !! o), (m2 !! o); simplify_equality'; f_equal; auto.
-    naive_solver auto using seps_union_half_distr.
-  * sep_unfold; intros [m] ????; simplify_map_equality'.
-  * done.
-  * sep_unfold; intros [m1] [m2] ? Hm; simplify_equality'. apply map_empty.
-    intros o. specialize (Hm o); simplify_map_equality. by destruct (m1 !! o).
-  * sep_unfold; intros [m1] [m2] ???; simpl in *; subst.
-    by rewrite (left_id_L ∅ (union_with _)).
-  * sep_unfold; intros [m]. split; [done|].
-    intros [? Hm]. destruct (sep_inhabited A) as (x&?&?).
-    specialize (Hm (Map {[fresh (dom _ m), [x]]}));
-      feed specialize Hm; [|simplify_map_equality'].
-    intros o. destruct (m !! o) as [w|] eqn:Hw; simplify_map_equality'.
-    { rewrite lookup_singleton_ne; eauto. intros <-.
-      eapply (is_fresh (dom indexset m)), fin_map_dom.elem_of_dom_2; eauto. }
-    destruct ({[_]} !! _) eqn:?; simplify_map_equality; split.
-    + by rewrite Forall_singleton.
-    + by inversion_clear 1; decompose_Forall_hyps'.
-Qed.
diff --git a/theories/mapset.v b/theories/mapset.v
index 6798d12d7c07ee59c2a25b7fd461ea8bb8a19d84..ab11a9f6d39c9e51d0f6fe665b36c40983521e44 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -5,27 +5,28 @@ elements of the unit type. Since maps enjoy extensional equality, the
 constructed finite sets do so as well. *)
 Require Export fin_map_dom.
 
-Record mapset (M : Type → Type) := Mapset { mapset_car: M unit }.
+Record mapset (Mu : Type) := Mapset { mapset_car: Mu }.
 Arguments Mapset {_} _.
 Arguments mapset_car {_} _.
 
 Section mapset.
 Context `{FinMap K M}.
 
-Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
+Instance mapset_elem_of: ElemOf K (mapset (M unit)) := λ x X,
   mapset_car X !! x = Some ().
-Instance mapset_empty: Empty (mapset M) := Mapset ∅.
-Instance mapset_singleton: Singleton K (mapset M) := λ x, Mapset {[ (x,()) ]}.
-Instance mapset_union: Union (mapset M) := λ X1 X2,
+Instance mapset_empty: Empty (mapset (M unit)) := Mapset ∅.
+Instance mapset_singleton: Singleton K (mapset (M unit)) := λ x,
+  Mapset {[ (x,()) ]}.
+Instance mapset_union: Union (mapset (M unit)) := λ X1 X2,
   let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∪ m2).
-Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
+Instance mapset_intersection: Intersection (mapset (M unit)) := λ X1 X2,
   let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∩ m2).
-Instance mapset_difference: Difference (mapset M) := λ X1 X2,
+Instance mapset_difference: Difference (mapset (M unit)) := λ X1 X2,
   let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∖ m2).
-Instance mapset_elems: Elements K (mapset M) := λ X,
+Instance mapset_elems: Elements K (mapset (M unit)) := λ X,
   let (m) := X in fst <$> map_to_list m.
 
-Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2.
+Lemma mapset_eq (X1 X2 : mapset (M unit)) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2.
 Proof.
   split; [by intros ->|].
   destruct X1 as [m1], X2 as [m2]. simpl. intros E.
@@ -33,16 +34,17 @@ Proof.
 Qed.
 
 Global Instance mapset_eq_dec `{∀ m1 m2 : M unit, Decision (m1 = m2)}
-  (X1 X2 : mapset M) : Decision (X1 = X2) | 1.
+  (X1 X2 : mapset (M unit)) : Decision (X1 = X2) | 1.
 Proof.
  refine
   match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end;
   abstract congruence.
 Defined.
-Global Instance mapset_elem_of_dec x (X : mapset M) : Decision (x ∈ X) | 1.
+Global Instance mapset_elem_of_dec x (X : mapset (M unit)) :
+  Decision (x ∈ X) | 1.
 Proof. solve_decision. Defined.
 
-Instance: Collection K (mapset M).
+Instance: Collection K (mapset (M unit)).
 Proof.
   split; [split | | ].
   * unfold empty, elem_of, mapset_empty, mapset_elem_of.
@@ -61,9 +63,9 @@ Proof.
     intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
     destruct (m2 !! x) as [[]|]; intuition congruence.
 Qed.
-Global Instance: PartialOrder (@subseteq (mapset M) _).
+Global Instance: PartialOrder (@subseteq (mapset (M unit)) _).
 Proof. split; try apply _. intros ????. apply mapset_eq. intuition. Qed.
-Global Instance: FinCollection K (mapset M).
+Global Instance: FinCollection K (mapset (M unit)).
 Proof.
   split.
   * apply _.
@@ -75,14 +77,15 @@ Proof.
     apply NoDup_fst_map_to_list.
 Qed.
 
-Definition mapset_map_with {A B} (f: bool → A → B) (X : mapset M) : M A → M B :=
+Definition mapset_map_with {A B} (f: bool → A → B)
+    (X : mapset (M unit)) : M A → M B :=
   let (m) := X in merge (λ x y,
     match x, y with
     | Some _, Some a => Some (f true a)
     | None, Some a => Some (f false a)
     | _, None => None
     end) m.
-Definition mapset_dom_with {A} (f : A → bool) (m : M A) : mapset M :=
+Definition mapset_dom_with {A} (f : A → bool) (m : M A) : mapset (M unit) :=
   Mapset $ merge (λ x _,
     match x with
     | Some a => if f a then Some () else None
@@ -105,8 +108,9 @@ Proof.
   * naive_solver.
 Qed.
 
-Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
-Instance mapset_dom_spec: FinMapDom K M (mapset M).
+Instance mapset_dom {A} : Dom (M A) (mapset (M unit)) :=
+  mapset_dom_with (λ _, true).
+Instance mapset_dom_spec: FinMapDom K M (mapset (M unit)).
 Proof.
   split; try apply _. intros. unfold dom, mapset_dom.
   rewrite elem_of_mapset_dom_with. unfold is_Some. naive_solver.
diff --git a/theories/natmap.v b/theories/natmap.v
index 1672c76934d13e7d80191792a51ad75d17378045..3daa5426af6edbbee3681443bc27c1a5aadc89df 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -23,11 +23,29 @@ Proof.
   intros ->. by destruct Hwf.
 Qed.
 
-Definition natmap (A : Type) : Type := sig (@natmap_wf A).
+Record natmap (A : Type) : Type := NatMap {
+  natmap_car : natmap_raw A;
+  natmap_prf : natmap_wf natmap_car
+}.
+Arguments NatMap {_} _ _.
+Arguments natmap_car {_} _.
+Arguments natmap_prf {_} _.
+Lemma natmap_eq {A} (m1 m2 : natmap A) :
+  m1 = m2 ↔ natmap_car m1 = natmap_car m2.
+Proof.
+  split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
+  simplify_equality'; f_equal; apply proof_irrel.
+Qed.
+Global Instance natmap_eq_dec `{∀ x y : A, Decision (x = y)}
+    (m1 m2 : natmap A) : Decision (m1 = m2) :=
+  match decide (natmap_car m1 = natmap_car m2) with
+  | left H => left (proj2 (natmap_eq m1 m2) H)
+  | right H => right (H ∘ proj1 (natmap_eq m1 m2))
+  end.
 
-Instance natmap_empty {A} : Empty (natmap A) := [] ↾ I.
-Instance natmap_lookup {A} : Lookup nat A (natmap A) :=
-  λ i m, match m with exist l _ => mjoin (l !! i) end.
+Instance natmap_empty {A} : Empty (natmap A) := NatMap [] I.
+Instance natmap_lookup {A} : Lookup nat A (natmap A) := λ i m,
+  let (l,_) := m in mjoin (l !! i).
 
 Fixpoint natmap_singleton_raw {A} (i : nat) (x : A) : natmap_raw A :=
   match i with 0 => [Some x]| S i => None :: natmap_singleton_raw i x end.
@@ -75,7 +93,7 @@ Proof.
     eauto using natmap_singleton_wf, natmap_cons_canon_wf, natmap_wf_inv.
 Qed.
 Instance natmap_alter {A} : PartialAlter nat A (natmap A) := λ f i m,
-  match m with exist l Hl => _↾natmap_alter_wf f i l Hl end.
+  let (l,Hl) := m in NatMap _ (natmap_alter_wf f i l Hl).
 Lemma natmap_lookup_alter_raw {A} (f : option A → option A) i l :
   mjoin (natmap_alter_raw f i l !! i) = f (mjoin (l !! i)).
 Proof.
@@ -103,8 +121,8 @@ Proof.
   revert i. induction l; intros [|?]; simpl; autorewrite with natmap; auto.
 Qed.
 Hint Rewrite @natmap_lookup_omap_raw : natmap.
-Global Instance natmap_omap: OMap natmap := λ A B f l,
-  _ ↾ natmap_omap_raw_wf f _ (proj2_sig l).
+Global Instance natmap_omap: OMap natmap := λ A B f m,
+  let (l,Hl) := m in NatMap _ (natmap_omap_raw_wf f _ Hl).
 
 Definition natmap_merge_raw {A B C} (f : option A → option B → option C) :
     natmap_raw A → natmap_raw B → natmap_raw C :=
@@ -130,7 +148,7 @@ Proof.
 Qed.
 Instance natmap_merge: Merge natmap := λ A B C f m1 m2,
   let (l1, Hl1) := m1 in let (l2, Hl2) := m2 in
-  natmap_merge_raw f _ _ ↾ natmap_merge_wf _ _ _ Hl1 Hl2.
+  NatMap (natmap_merge_raw f l1 l2) (natmap_merge_wf _ _ _ Hl1 Hl2).
 
 Fixpoint natmap_to_list_raw {A} (i : nat) (l : natmap_raw A) : list (nat * A) :=
   match l with
@@ -171,7 +189,7 @@ Proof.
   rewrite natmap_elem_of_to_list_raw_aux. intros (?&?&?). lia.
 Qed.
 Instance natmap_to_list {A} : FinMapToList nat A (natmap A) := λ m,
-  match m with exist l _ => natmap_to_list_raw 0 l end.
+  let (l,_) := m in natmap_to_list_raw 0 l.
 
 Definition natmap_map_raw {A B} (f : A → B) : natmap_raw A → natmap_raw B :=
   fmap (fmap f).
@@ -187,13 +205,13 @@ Proof.
   unfold natmap_map_raw. rewrite list_lookup_fmap. by destruct (l !! i).
 Qed.
 Instance natmap_map: FMap natmap := λ A B f m,
-  natmap_map_raw f _ ↾ natmap_map_wf _ _ (proj2_sig m).
+  let (l,Hl) := m in NatMap (natmap_map_raw f l) (natmap_map_wf _ _ Hl).
 
 Instance: FinMap nat natmap.
 Proof.
   split.
   * unfold lookup, natmap_lookup. intros A [l1 Hl1] [l2 Hl2] E.
-    apply (sig_eq_pi _). revert l2 Hl1 Hl2 E. simpl.
+    apply natmap_eq. revert l2 Hl1 Hl2 E. simpl.
     induction l1 as [|[x|] l1 IH]; intros [|[y|] l2] Hl1 Hl2 E; simpl in *.
     + done.
     + by specialize (E 0).
@@ -225,7 +243,7 @@ Proof.
   induction (reverse l) as [|[]]; simpl; eauto.
 Qed.
 Definition list_to_natmap {A} (l : list (option A)) : natmap A :=
-  reverse (strip_Nones (reverse l)) ↾ list_to_natmap_wf l.
+  NatMap (reverse (strip_Nones (reverse l))) (list_to_natmap_wf l).
 Lemma list_to_natmap_spec {A} (l : list (option A)) i :
   list_to_natmap l !! i = mjoin (l !! i).
 Proof.
@@ -237,7 +255,7 @@ Proof.
 Qed.
 
 (** Finally, we can construct sets of [nat]s satisfying extensional equality. *)
-Notation natset := (mapset natmap).
+Notation natset := (mapset (natmap unit)).
 Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
 Instance: FinMapDom nat natmap natset := mapset_dom_spec.
 
@@ -245,7 +263,8 @@ Instance: FinMapDom nat natmap natset := mapset_dom_spec.
 Fixpoint of_bools (βs : list bool) : natset :=
   Mapset $ list_to_natmap $ (λ β : bool, if β then Some () else None) <$> βs.
 Definition to_bools (X : natset) : list bool :=
-  (λ mu, match mu with Some _ => true | None => false end) <$> ` (mapset_car X).
+  (λ mu, match mu with Some _ => true | None => false end)
+    <$> natmap_car (mapset_car X).
 
 Lemma of_bools_unfold βs :
   of_bools βs
@@ -278,14 +297,14 @@ Qed.
 
 (** A [natmap A] forms a stack with elements of type [A] and possible holes *)
 Definition natmap_push {A} (o : option A) (m : natmap A) : natmap A :=
-  match m with exist l Hl => _↾natmap_cons_canon_wf o l Hl end.
+  let (l,Hl) := m in NatMap _ (natmap_cons_canon_wf o l Hl).
 
 Definition natmap_pop_raw {A} (l : natmap_raw A) : natmap_raw A := tail l.
 Lemma natmap_pop_wf {A} (l : natmap_raw A) :
   natmap_wf l → natmap_wf (natmap_pop_raw l).
 Proof. destruct l; simpl; eauto using natmap_wf_inv. Qed.
 Definition natmap_pop {A} (m : natmap A) : natmap A :=
-  match m with exist l Hl => _↾natmap_pop_wf _ Hl end.
+  let (l,Hl) := m in NatMap _ (natmap_pop_wf _ Hl).
 
 Lemma lookup_natmap_push_O {A} o (m : natmap A) : natmap_push o m !! 0 = o.
 Proof. by destruct o, m as [[|??]]. Qed.
@@ -303,4 +322,4 @@ Proof.
   * by rewrite lookup_natmap_push_S, lookup_natmap_pop.
 Qed.
 Lemma natmap_pop_push {A} o (m : natmap A) : natmap_pop (natmap_push o m) = m.
-Proof. apply (sig_eq_pi _). by destruct o, m as [[|??]]. Qed.
+Proof. apply natmap_eq. by destruct o, m as [[|??]]. Qed.
diff --git a/theories/nmap.v b/theories/nmap.v
index 66cbb0a456e5349f99c187f453aaed779495e1de..37e71d372a1d1d8d2543cc9b4042951ad9dffd4e 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -81,6 +81,6 @@ Qed.
 
 (** * Finite sets *)
 (** We construct sets of [N]s satisfying extensional equality. *)
-Notation Nset := (mapset Nmap).
+Notation Nset := (mapset (Nmap unit)).
 Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
 Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
diff --git a/theories/numbers.v b/theories/numbers.v
index 9ac7c50f8282961e0e341cf23db1b4c565761057..84a7ce61ccf53e0051be84258193a4cf4d278752 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -179,10 +179,11 @@ Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%N : N_scope.
 Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%N : N_scope.
 Notation "(≤)" := N.le (only parsing) : N_scope.
 Notation "(<)" := N.lt (only parsing) : N_scope.
-
 Infix "`div`" := N.div (at level 35) : N_scope.
 Infix "`mod`" := N.modulo (at level 35) : N_scope.
 
+Arguments N.add _ _ : simpl never.
+
 Instance: Injective (=) (=) Npos.
 Proof. by injection 1. Qed.
 
diff --git a/theories/option.v b/theories/option.v
index 189702d25e027edbecd1f08cdbaf59942aa04aeb..4df5d7e2371655f84ae2e322ca51e41e3a343b40 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -97,6 +97,10 @@ Instance option_join: MJoin option := λ A x,
 Instance option_fmap: FMap option := @option_map.
 Instance option_guard: MGuard option := λ P dec A x,
   match dec with left H => x H | _ => None end.
+Definition maybe_inl {A B} (xy : A + B) : option A :=
+  match xy with inl x => Some x | _ => None end.
+Definition maybe_inr {A B} (xy : A + B) : option B :=
+  match xy with inr y => Some y | _ => None end.
 
 Lemma fmap_is_Some {A B} (f : A → B) x : is_Some (f <$> x) ↔ is_Some x.
 Proof. unfold is_Some; destruct x; naive_solver. Qed.
@@ -118,7 +122,7 @@ Lemma option_bind_assoc {A B C} (f : A → option B)
 Proof. by destruct x; simpl. Qed.
 Lemma option_bind_ext {A B} (f g : A → option B) x y :
   (∀ a, f a = g a) → x = y → x ≫= f = y ≫= g.
-Proof. intros. destruct x, y; simplify_equality; simpl; auto. Qed.
+Proof. intros. destruct x, y; simplify_equality; csimpl; auto. Qed.
 Lemma option_bind_ext_fun {A B} (f g : A → option B) x :
   (∀ a, f a = g a) → x ≫= f = x ≫= g.
 Proof. intros. by apply option_bind_ext. Qed.
@@ -192,11 +196,7 @@ Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
   | _ => rewrite option_guard_False by tac
   end.
 Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
-  let assert_Some_None A o H := first
-    [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x;
-      assert (o = Some x') as H by tac
-    | assert (o = None) as H by tac ]
-  in repeat match goal with
+  repeat match goal with
   | _ => progress simplify_equality'
   | _ => progress simpl_option_monad by tac
   | H : mbind (M:=option) _ ?o = ?x |- _ =>
diff --git a/theories/orders.v b/theories/orders.v
index 8f4599c4becdebdfaff8db2978f0e1bbe704fec0..0a98b2e043282f6fa96980578f590a646d0b1b4c 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -214,7 +214,7 @@ Section sorted.
     (∀ x y, R1 x y → R2 (f x) (f y)) →
     StronglySorted R1 l → StronglySorted R2 (f <$> l).
   Proof.
-    induction 2; simpl; constructor;
+    induction 2; csimpl; constructor;
       rewrite ?Forall_fmap; eauto using Forall_impl.
   Qed.
 End sorted.
diff --git a/theories/pmap.v b/theories/pmap.v
index a58393bd8270d665937120ebc2be523b7faa3ee9..2208a9b0e1fc18671430ec4a0ad45f3128aee07c 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -70,19 +70,32 @@ Defined.
 
 (** Now we restrict the data type of trees to those that are well formed and
 thereby obtain a data type that ensures canonicity. *)
-Definition Pmap A := dsig (@Pmap_wf A).
+Inductive Pmap A := PMap {
+  pmap_car : Pmap_raw A;
+  pmap_bool_prf : bool_decide (Pmap_wf pmap_car)
+}.
+Arguments PMap {_} _ _.
+Arguments pmap_car {_} _.
+Arguments pmap_bool_prf {_} _.
+Definition PMap' {A} (t : Pmap_raw A) (p : Pmap_wf t) : Pmap A :=
+  PMap t (bool_decide_pack _ p).
+Definition pmap_prf {A} (m : Pmap A) : Pmap_wf (pmap_car m) :=
+  bool_decide_unpack _ (pmap_bool_prf m).
+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_equality'; f_equal; apply proof_irrel.
+Qed.
 
 (** * Operations on the data structure *)
-Global Instance Pmap_eq_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) :
-    Decision (t1 = t2) :=
-  match Pmap_raw_eq_dec (`t1) (`t2) with
-  | left H => left (proj2 (dsig_eq _ t1 t2) H)
-  | right H => right (H ∘ proj1 (dsig_eq _ t1 t2))
+Global Instance Pmap_eq_dec `{∀ x y : A, Decision (x = y)}
+    (m1 m2 : Pmap A) : Decision (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.
-
 Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
-Global Instance Pempty {A} : Empty (Pmap A) :=
-  (∅ : Pmap_raw A) ↾ bool_decide_pack _ Pmap_wf_leaf.
+Global Instance Pempty {A} : Empty (Pmap A) := PMap' ∅ Pmap_wf_leaf.
 
 Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
   fix go (i : positive) (t : Pmap_raw A) {struct t} : option A :=
@@ -93,7 +106,7 @@ Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
      | 1 => o | i~0 => @lookup _ _ _ go i l | i~1 => @lookup _ _ _ go i r
      end
   end.
-Instance Plookup {A} : Lookup positive A (Pmap A) := λ i t, `t !! i.
+Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
 
 Lemma Plookup_empty {A} i : (∅ : Pmap_raw A) !! i = None.
 Proof. by destruct i. Qed.
@@ -193,8 +206,8 @@ Proof.
   * intros [?|?|]; simpl; intuition.
   * intros [?|?|]; simpl; intuition.
 Qed.
-Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i t,
-  dexist (partial_alter f i (`t)) (Ppartial_alter_wf f i _ (proj2_dsig t)).
+Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
+  PMap' (partial_alter f i (pmap_car m)) (Ppartial_alter_wf f i _ (pmap_prf m)).
 Lemma Plookup_alter {A} f i (t : Pmap_raw A) :
   partial_alter f i t !! i = f (t !! i).
 Proof.
@@ -215,18 +228,18 @@ Proof.
   * intros [?|?|] [?|?|]; simpl; PNode_canon_rewrite; auto; congruence.
 Qed.
 
-Instance Pfmap_raw {A B} (f : A → B) : FMapD Pmap_raw f :=
-  fix go (t : Pmap_raw A) := let _ : FMapD _ _ := @go in
+Instance Pfmap_raw : FMap Pmap_raw := λ A B f,
+  fix go t :=
   match t with
-  | PLeaf => PLeaf | PNode l x r => PNode (f <$> l) (f <$> x) (f <$> r)
+  | PLeaf => PLeaf | PNode l x r => PNode (go l) (f <$> x) (go r)
   end.
 Lemma Pfmap_ne `(f : A → B) (t : Pmap_raw A) : Pmap_ne t → Pmap_ne (fmap f t).
-Proof. induction 1; simpl; auto. Qed.
+Proof. induction 1; csimpl; auto. Qed.
 Local Hint Resolve Pfmap_ne.
 Lemma Pfmap_wf `(f : A → B) (t : Pmap_raw A) : Pmap_wf t → Pmap_wf (fmap f t).
-Proof. induction 1; simpl; intuition. Qed.
-Global Instance Pfmap {A B} (f : A → B) : FMapD Pmap f := λ t,
-  dexist _ (Pfmap_wf f _ (proj2_dsig t)).
+Proof. induction 1; csimpl; intuition. Qed.
+Global Instance Pfmap : FMap Pmap := λ A B f m,
+  PMap' (f <$> pmap_car m) (Pfmap_wf f _ (pmap_prf m)).
 Lemma Plookup_fmap {A B} (f : A → B) (t : Pmap_raw A) i :
   (f <$> t) !! i = f <$> t !! i.
 Proof. revert i. induction t. done. by intros [?|?|]; simpl. Qed.
@@ -305,26 +318,26 @@ Proof.
    apply IHr; auto. intros i x Hi.
    apply (Hin (i~1) x). by rewrite Preverse_xI, (associative_L _) in Hi.
 Qed.
-Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) :=
-  λ t, Pto_list_raw 1 (`t) [].
+Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
+  Pto_list_raw 1 (pmap_car m) [].
 
-Instance Pomap_raw {A B} (f : A → option B) : OMapD Pmap_raw f :=
-  fix go (t : Pmap_raw A) := let _ : OMapD _ _ := @go in
+Instance Pomap_raw : OMap Pmap_raw := λ A B f,
+  fix go t :=
   match t with
-  | PLeaf => PLeaf | PNode l o r => PNode_canon (omap f l) (o ≫= f) (omap f r)
+  | PLeaf => PLeaf | PNode l o r => PNode_canon (go l) (o ≫= f) (go r)
   end.
 Lemma Pomap_wf {A B} (f : A → option B) (t : Pmap_raw A) :
   Pmap_wf t → Pmap_wf (omap f t).
-Proof. induction 1; simpl; auto. Qed.
+Proof. induction 1; csimpl; auto. Qed.
 Local Hint Resolve Pomap_wf.
 Lemma Pomap_lookup {A B} (f : A → option B) (t : Pmap_raw A) i :
   omap f t !! i = t !! i ≫= f.
 Proof.
   revert i. induction t as [| l IHl o r IHr ]; [done |].
-  intros [?|?|]; simpl; PNode_canon_rewrite; auto.
+  intros [?|?|]; csimpl; PNode_canon_rewrite; auto.
 Qed.
-Global Instance Pomap: OMap Pmap := λ A B f t,
-  dexist _ (Pomap_wf f _ (proj2_dsig t)).
+Global Instance Pomap: OMap Pmap := λ A B f m,
+  PMap' (omap f (pmap_car m)) (Pomap_wf f _ (pmap_prf m)).
 
 Instance Pmerge_raw : Merge Pmap_raw :=
   fix Pmerge_raw A B C f t1 t2 : Pmap_raw C :=
@@ -339,8 +352,8 @@ Local Arguments omap _ _ _ _ _ _ : simpl never.
 Lemma Pmerge_wf {A B C} (f : option A → option B → option C) t1 t2 :
   Pmap_wf t1 → Pmap_wf t2 → Pmap_wf (merge f t1 t2).
 Proof. intros t1wf. revert t2. induction t1wf; destruct 1; simpl; auto. Qed.
-Global Instance Pmerge: Merge Pmap := λ A B C f t1 t2,
-  dexist _ (Pmerge_wf f _ _ (proj2_dsig t1) (proj2_dsig t2)).
+Global Instance Pmerge: Merge Pmap := λ A B C f m1 m2,
+  PMap' _ (Pmerge_wf f _ _ (pmap_prf m1) (pmap_prf m2)).
 Lemma Pmerge_spec {A B C} (f : option A → option B → option C)
     (Hf : f None None = None) (t1 : Pmap_raw A) t2 i :
   merge f t1 t2 !! i = f (t1 !! i) (t2 !! i).
@@ -357,7 +370,7 @@ Qed.
 Global Instance: FinMap positive Pmap.
 Proof.
   split.
-  * intros ? [t1 ?] [t2 ?] ?. apply dsig_eq; simpl.
+  * intros ? [t1 ?] [t2 ?] ?. apply Pmap_eq; simpl.
     apply Pmap_wf_eq_get; trivial; by apply (bool_decide_unpack _).
   * by intros ? [].
   * intros ?? [??] ?. by apply Plookup_alter.
@@ -374,6 +387,6 @@ Qed.
 
 (** * Finite sets *)
 (** We construct sets of [positives]s satisfying extensional equality. *)
-Notation Pset := (mapset Pmap).
+Notation Pset := (mapset (Pmap unit)).
 Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
 Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
diff --git a/theories/tactics.v b/theories/tactics.v
index 04111e478d8c2a39d08b69563636eda5760f44ae..9d9e5aabca407b0aa6a2f82b93a67bb1f836426c 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -139,6 +139,10 @@ into [H: blocked T], where [blocked] is the identity function. If a hypothesis
 is already blocked, it will not be blocked again. The tactic [unblock_hyps]
 removes [blocked] everywhere. *)
 
+Ltac block_hyp H :=
+  lazymatch type of H with
+  | block _ => idtac | ?T => change T with (block T) in H
+  end.
 Ltac block_hyps := repeat_on_hyps (fun H =>
   match type of H with block _ => idtac | ?T => change (block T) in H end).
 Ltac unblock_hyps := unfold block in * |-.
@@ -149,6 +153,46 @@ Ltac injection' H := block_goal; injection H; clear H; intros; unblock_goal.
 
 (** The tactic [simplify_equality] repeatedly substitutes, discriminates,
 and injects equalities, and tries to contradict impossible inequalities. *)
+Ltac fold_classes :=
+  repeat match goal with
+  | |- appcontext [ ?F ] =>
+    progress match type of F with
+    | FMap _ =>
+       change F with (@fmap _ F);
+       repeat change (@fmap _ (@fmap _ F)) with (@fmap _ F)
+    | MBind _ =>
+       change F with (@mbind _ F);
+       repeat change (@mbind _ (@mbind _ F)) with (@mbind _ F)
+    | OMap _ =>
+       change F with (@omap _ F);
+       repeat change (@omap _ (@omap _ F)) with (@omap _ F)
+    | Alter _ _ _ =>
+       change F with (@alter _ _ _ F);
+       repeat change (@alter _ _ _ (@alter _ _ _ F)) with (@alter _ _ _ F)
+    end
+  end.
+Ltac fold_classes_hyps :=
+  repeat match goal with
+  | _ : appcontext [ ?F ] |- _ =>
+    progress match type of F with
+    | FMap _ =>
+       change F with (@fmap _ F) in *;
+       repeat change (@fmap _ (@fmap _ F)) with (@fmap _ F) in *
+    | MBind _ =>
+       change F with (@mbind _ F) in *;
+       repeat change (@mbind _ (@mbind _ F)) with (@mbind _ F) in *
+    | OMap _ =>
+       change F with (@omap _ F) in *;
+       repeat change (@omap _ (@omap _ F)) with (@omap _ F) in *
+    | Alter _ _ _ =>
+       change F with (@alter _ _ _ F) in *;
+       repeat change (@alter _ _ _ (@alter _ _ _ F)) with (@alter _ _ _ F) in *
+    end
+  end.
+Tactic Notation "csimpl" "in" "*" :=
+  try (progress simpl in *; fold_classes; fold_classes_hyps).
+Tactic Notation "csimpl" := try (progress simpl; fold_classes).
+
 Ltac simplify_equality := repeat
   match goal with
   | H : _ ≠ _ |- _ => by destruct H
@@ -166,8 +210,8 @@ Ltac simplify_equality := repeat
     assert (y = x) by congruence; clear H2
   | H1 : ?o = Some ?x, H2 : ?o = None |- _ => congruence
   end.
-Ltac simplify_equality' := repeat (progress simpl in * || simplify_equality).
-Ltac f_equal' := simpl in *; f_equal.
+Ltac simplify_equality' := repeat (progress csimpl in * || simplify_equality).
+Ltac f_equal' := csimpl in *; f_equal.
 
 (** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2]
 runs [tac x] for each element [x] until [tac x] succeeds. If it does not
diff --git a/theories/zmap.v b/theories/zmap.v
index 605be57194f82a01643401087e2b709bcab1e50b..ac098a51dea9ca014e5b199085a9f4948319ae78 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -43,7 +43,8 @@ Instance Zomap: OMap Zmap := λ A B f t,
   match t with ZMap o t t' => ZMap (o ≫= f) (omap f t) (omap f t') end.
 Instance Zmerge: Merge Zmap := λ A B C f t1 t2,
   match t1, t2 with
-  | ZMap o1 t1 t1', ZMap o2 t2 t2' => ZMap (f o1 o2) (merge f t1 t2) (merge f t1' t2')
+  | ZMap o1 t1 t1', ZMap o2 t2 t2' =>
+     ZMap (f o1 o2) (merge f t1 t2) (merge f t1' t2')
   end.
 Instance Nfmap: FMap Zmap := λ A B f t,
   match t with ZMap o t t' => ZMap (f <$> o) (f <$> t) (f <$> t') end.
@@ -91,6 +92,6 @@ Qed.
 
 (** * Finite sets *)
 (** We construct sets of [Z]s satisfying extensional equality. *)
-Notation Zset := (mapset Zmap).
+Notation Zset := (mapset (Zmap unit)).
 Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
 Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.