diff --git a/theories/base.v b/theories/base.v
index 7064c776235b31314c1273ab99903fcc9151e396..d2b78fb670322c1af2ec66a373a1f0d5f60b364b 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -9,11 +9,6 @@ Global Set Automatic Coercions Import.
 Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
 
 (** * General *)
-(** The following coercion allows us to use Booleans as propositions. *)
-Coercion Is_true : bool >-> Sortclass.
-Notation "(&&)" := andb (only parsing).
-Notation "(||)" := orb (only parsing).
-
 (** Zipping lists. *)
 Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :=
   fix go l1 l2 :=
@@ -500,14 +495,6 @@ Class Merge (M : Type → Type) :=
 Instance: Params (@merge) 4.
 Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch.
 
-(** We lift the insert and delete operation to lists of elements. *)
-Definition insert_list `{Insert K A M} (l : list (K * A)) (m : M) : M :=
-  fold_right (λ p, <[p.1:=p.2]>) m l.
-Instance: Params (@insert_list) 4.
-Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
-  fold_right delete m l.
-Instance: Params (@delete_list) 3.
-
 (** The function [union_with f m1 m2] is supposed to yield the union of [m1]
 and [m2] using the function [f] to combine values of members that are in
 both [m1] and [m2]. *)
@@ -724,8 +711,8 @@ Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C,
     Union C, Intersection C, Difference C,
     Elements A C, ∀ x y : A, Decision (x = y)} : Prop := {
   fin_collection :>> Collection A C;
-  elements_spec X x : x ∈ X ↔ x ∈ elements X;
-  elements_nodup X : NoDup (elements X)
+  elem_of_elements X x : x ∈ elements X ↔ x ∈ X;
+  NoDup_elements X : NoDup (elements X)
 }.
 Class Size C := size: C → nat.
 Arguments size {_ _} !_ / : simpl nomatch.
@@ -763,6 +750,20 @@ Class FreshSpec A C `{ElemOf A C,
   is_fresh (X : C) : fresh X ∉ X
 }.
 
+(** * Booleans *)
+(** The following coercion allows us to use Booleans as propositions. *)
+Coercion Is_true : bool >-> Sortclass.
+Notation "(&&)" := andb (only parsing).
+Notation "(||)" := orb (only parsing).
+Infix "&&*" := (zip_with (&&)) (at level 40).
+Infix "||*" := (zip_with (||)) (at level 50).
+
+Definition bool_le (β1 β2 : bool) : Prop := negb β1 || β2.
+Infix "=.>" := bool_le (at level 70).
+Infix "=.>*" := (Forall2 bool_le) (at level 70).
+Instance: PartialOrder bool_le.
+Proof. repeat split; repeat intros [|]; compute; tauto. Qed.
+
 (** * Miscellaneous *)
 Class Half A := half: A → A.
 Notation "½" := half : C_scope.
@@ -823,14 +824,6 @@ Section prod_relation.
 End prod_relation.
 
 (** ** Other *)
-Definition proj_eq {A B} (f : B → A) : relation B := λ x y, f x = f y.
-Global Instance proj_eq_equivalence `(f : B → A) : Equivalence (proj_eq f).
-Proof. unfold proj_eq. repeat split; red; intuition congruence. Qed.
-Notation "x ~{ f } y" := (proj_eq f x y)
-  (at level 70, format "x  ~{ f }  y") : C_scope.
-Hint Extern 0 (_ ~{_} _) => reflexivity.
-Hint Extern 0 (_ ~{_} _) => symmetry; assumption.
-
 Instance: ∀ A B (x : B), Commutative (=) (λ _ _ : A, x).
 Proof. red. trivial. Qed.
 Instance: ∀ A (x : A), Associative (=) (λ _ _ : A, x).
diff --git a/theories/collections.v b/theories/collections.v
index c3dd894fb24a5d95e1e94c0b5f505400b1f33021..e59828b9e3f34426c691cceb3d99f0c97a70242e 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -18,10 +18,8 @@ Section simple_collection.
   Proof. intros. apply elem_of_union. auto. Qed.
   Lemma elem_of_union_r x X Y : x ∈ Y → x ∈ X ∪ Y.
   Proof. intros. apply elem_of_union. auto. Qed.
-
   Global Instance: BoundedJoinSemiLattice C.
   Proof. firstorder auto. Qed.
-
   Lemma elem_of_subseteq X Y : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y.
   Proof. done. Qed.
   Lemma elem_of_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
@@ -31,7 +29,12 @@ Section simple_collection.
   Proof. firstorder. Qed.
   Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X.
   Proof. firstorder. Qed.
-
+  Lemma collection_positive_l X Y : X ∪ Y ≡ ∅ → X ≡ ∅.
+  Proof.
+    rewrite !elem_of_equiv_empty. setoid_rewrite elem_of_union. naive_solver.
+  Qed.
+  Lemma collection_positive_l_alt X Y : X ≢ ∅ → X ∪ Y ≢ ∅.
+  Proof. eauto using collection_positive_l. Qed.
   Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X.
   Proof.
     split.
@@ -42,7 +45,6 @@ Section simple_collection.
   Proof. by repeat intro; subst. Qed.
   Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈) | 5.
   Proof. intros ???; subst. firstorder. Qed.
-
   Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
   Proof.
     split.
@@ -51,7 +53,6 @@ Section simple_collection.
     * intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
       intros. apply elem_of_union_r; auto.
   Qed.
-
   Lemma non_empty_singleton x : {[ x ]} ≢ ∅.
   Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.
   Lemma not_elem_of_singleton x y : x ∉ {[ y ]} ↔ x ≠ y.
@@ -68,6 +69,10 @@ Section simple_collection.
     Proof. unfold_leibniz. apply elem_of_equiv_alt. Qed.
     Lemma elem_of_equiv_empty_L X : X = ∅ ↔ ∀ x, x ∉ X.
     Proof. unfold_leibniz. apply elem_of_equiv_empty. Qed.
+    Lemma collection_positive_l_L X Y : X ∪ Y = ∅ → X = ∅.
+    Proof. unfold_leibniz. apply collection_positive_l. Qed.
+    Lemma collection_positive_l_alt_L X Y : X ≠ ∅ → X ∪ Y ≠ ∅.
+    Proof. unfold_leibniz. apply collection_positive_l_alt. Qed.
     Lemma non_empty_singleton_L x : {[ x ]} ≠ ∅.
     Proof. unfold_leibniz. apply non_empty_singleton. Qed.
   End leibniz.
@@ -385,7 +390,7 @@ Section quantifiers.
 End quantifiers.
 
 Section more_quantifiers.
-  Context `{Collection A B}.
+  Context `{SimpleCollection A B}.
 
   Lemma set_Forall_weaken (P Q : A → Prop) (Hweaken : ∀ x, P x → Q x) X :
     set_Forall P X → set_Forall Q X.
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 934413d40d7a431bfdc383a3e465e3285c774cc7..26ed4ae46289d672c9ad7969fb36f78b4c403552 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -6,8 +6,6 @@ principles on finite collections . *)
 Require Import Permutation ars listset.
 Require Export numbers collections.
 
-Definition collection_choose `{Elements A C} (X : C) : option A :=
-  head (elements X).
 Instance collection_size `{Elements A C} : Size C := length ∘ elements.
 Definition collection_fold `{Elements A C} {B}
   (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
@@ -18,76 +16,56 @@ Context `{FinCollection A C}.
 Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) elements.
 Proof.
   intros ?? E. apply NoDup_Permutation.
-  * apply elements_nodup.
-  * apply elements_nodup.
-  * intros. by rewrite <-!elements_spec, E.
+  * apply NoDup_elements.
+  * apply NoDup_elements.
+  * intros. by rewrite !elem_of_elements, E.
 Qed.
 Global Instance collection_size_proper: Proper ((≡) ==> (=)) size.
 Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
-
 Lemma size_empty : size (∅ : C) = 0.
 Proof.
   unfold size, collection_size. simpl.
   rewrite (elem_of_nil_inv (elements ∅)); [done |].
-  intro. rewrite <-elements_spec. solve_elem_of.
+  intro. rewrite elem_of_elements. solve_elem_of.
 Qed.
 Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
 Proof.
-  intros. apply equiv_empty. intro. rewrite elements_spec.
+  intros. apply equiv_empty. intro. rewrite <-elem_of_elements.
   rewrite (nil_length_inv (elements X)). by rewrite elem_of_nil. done.
 Qed.
 Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
 Proof. split. apply size_empty_inv. intros E. by rewrite E, size_empty. Qed.
 Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅.
 Proof. by rewrite size_empty_iff. Qed.
-
 Lemma size_singleton (x : A) : size {[ x ]} = 1.
 Proof.
   change (length (elements {[ x ]}) = length [x]).
   apply Permutation_length, NoDup_Permutation.
-  * apply elements_nodup.
+  * apply NoDup_elements.
   * apply NoDup_singleton.
-  * intros.
-    by rewrite <-elements_spec, elem_of_singleton, elem_of_list_singleton.
+  * intros. by rewrite elem_of_elements,
+      elem_of_singleton, elem_of_list_singleton.
 Qed.
 Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
-  unfold size, collection_size. simpl. rewrite !elements_spec.
+  unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
   generalize (elements X). intros [|? l]; intro; simplify_equality.
   rewrite (nil_length_inv l), !elem_of_list_singleton by done. congruence.
 Qed.
-
-Lemma collection_choose_Some X x : collection_choose X = Some x → x ∈ X.
-Proof.
-  unfold collection_choose. destruct (elements X) eqn:E; intros;
-    simplify_equality. rewrite elements_spec, E. by left.
-Qed.
-Lemma collection_choose_None X : collection_choose X = None → X ≡ ∅.
-Proof.
-  unfold collection_choose.
-  destruct (elements X) eqn:E; intros; simplify_equality.
-  apply equiv_empty. intros x. by rewrite elements_spec, E, elem_of_nil.
-Qed.
-Lemma elem_of_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
-Proof.
-  destruct (collection_choose X) eqn:?;
-    eauto using collection_choose_Some, collection_choose_None.
-Qed.
-Lemma collection_choose_is_Some X : X ≢ ∅ ↔ is_Some (collection_choose X).
-Proof.
-  destruct (collection_choose X) eqn:?.
-  * rewrite elem_of_equiv_empty. split; eauto using collection_choose_Some.
-  * split. intros []; eauto using collection_choose_None. by intros [??].
-Qed.
-Lemma not_elem_of_equiv_empty X : X ≢ ∅ ↔ (∃ x, x ∈ X).
+Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
 Proof.
-  destruct (elem_of_or_empty X) as [?|E]; [esolve_elem_of |].
-  setoid_rewrite E. setoid_rewrite elem_of_empty. naive_solver.
+  destruct (elements X) as [|x l] eqn:HX; [right|left].
+  * apply equiv_empty. intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
+  * exists x. rewrite <-elem_of_elements, HX. by left.
 Qed.
+Lemma collection_choose X : X ≢ ∅ → ∃ x, x ∈ X.
+Proof. intros. by destruct (collection_choose_or_empty X). Qed.
+Lemma collection_choose_L `{!LeibnizEquiv C} X : X ≠ ∅ → ∃ x, x ∈ X.
+Proof. unfold_leibniz. apply collection_choose. Qed.
 Lemma size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X.
 Proof.
-  intros E1. apply not_elem_of_equiv_empty. intros E2.
-  rewrite E2, size_empty in E1. lia.
+  intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|].
+  contradict Hsz. rewrite HX, size_empty; lia.
 Qed.
 Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}.
 Proof.
@@ -96,27 +74,24 @@ Proof.
   * rewrite elem_of_singleton. eauto using size_singleton_inv.
   * solve_elem_of.
 Qed.
-
 Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
 Proof.
   intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
   apply Permutation_length, NoDup_Permutation.
-  * apply elements_nodup.
-  * apply NoDup_app; repeat split; try apply elements_nodup.
-    intros x. rewrite <-!elements_spec. esolve_elem_of.
-  * intros. rewrite elem_of_app, <-!elements_spec. solve_elem_of.
+  * apply NoDup_elements.
+  * apply NoDup_app; repeat split; try apply NoDup_elements.
+    intros x. rewrite !elem_of_elements. esolve_elem_of.
+  * intros. rewrite elem_of_app, !elem_of_elements. solve_elem_of.
 Qed.
-
 Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
 Proof.
   refine (cast_if (decide_rel (∈) x (elements X)));
-    by rewrite (elements_spec _).
+    by rewrite <-(elem_of_elements _).
 Defined.
 Global Program Instance collection_subseteq_dec_slow (X Y : C) :
     Decision (X ⊆ Y) | 100 :=
   match decide_rel (=) (size (X ∖ Y)) 0 with
-  | left E1 => left _
-  | right E1 => right _
+  | left E1 => left _ | right E1 => right _
   end.
 Next Obligation.
   intros x Ex; apply dec_stable; intro. destruct (proj1 (elem_of_empty x)).
@@ -126,14 +101,12 @@ Next Obligation.
   intros E2. destruct E1. apply size_empty_iff, equiv_empty. intros x.
   rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
 Qed.
-
 Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
 Proof.
   rewrite <-size_union by solve_elem_of.
   setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by esolve_elem_of.
   rewrite <-union_difference, (commutative (∪)); solve_elem_of.
 Qed.
-
 Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
 Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
 Lemma subset_size X Y : X ⊂ Y → size X < size Y.
@@ -143,22 +116,19 @@ Proof.
   cut (size (Y ∖ X) ≠ 0); [lia |].
   by apply size_non_empty_iff, non_empty_difference.
 Qed.
-
 Lemma collection_wf : wf (strict (@subseteq C _)).
 Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
-
 Lemma collection_ind (P : C → Prop) :
   Proper ((≡) ==> iff) P →
   P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
 Proof.
   intros ? Hemp Hadd. apply well_founded_induction with (⊂).
   { apply collection_wf. }
-  intros X IH. destruct (elem_of_or_empty X) as [[x ?]|HX].
+  intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
   * rewrite (union_difference {[ x ]} X) by solve_elem_of.
     apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
   * by rewrite HX.
 Qed.
-
 Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
   Proper ((=) ==> (≡) ==> iff) P →
   P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
@@ -166,7 +136,8 @@ Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B)
 Proof.
   intros ? Hemp Hadd.
   cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X).
-  { intros help ?. apply help. apply elements_nodup. apply elements_spec. }
+  { intros help ?. apply help; [apply NoDup_elements|].
+    symmetry. apply elem_of_elements. }
   induction 1 as [|x l ?? IH]; simpl.
   * intros X HX. setoid_rewrite elem_of_nil in HX.
     rewrite equiv_empty. done. esolve_elem_of.
@@ -174,25 +145,23 @@ Proof.
     rewrite (union_difference {[ x ]} X) by esolve_elem_of.
     apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
 Qed.
-
 Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
     (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
     (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
   Proper ((≡) ==> R) (collection_fold f b).
 Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
-
 Global Instance set_Forall_dec `(P : A → Prop)
   `{∀ x, Decision (P x)} X : Decision (set_Forall P X) | 100.
 Proof.
   refine (cast_if (decide (Forall P (elements X))));
-    abstract (unfold set_Forall; setoid_rewrite elements_spec;
+    abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements;
       by rewrite <-Forall_forall).
 Defined.
 Global Instance set_Exists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X :
   Decision (set_Exists P X) | 100.
 Proof.
   refine (cast_if (decide (Exists P (elements X))));
-    abstract (unfold set_Exists; setoid_rewrite elements_spec;
+    abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements;
       by rewrite <-Exists_exists).
 Defined.
 Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X :
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 7c42a2668a308cfc2541ef5d1589029da8f49e02..66ce3e083eb889159e75b3b478bd8316adcfe97d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -35,7 +35,7 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
   lookup_partial_alter_ne {A} f (m : M A) i j :
     i ≠ j → partial_alter f i m !! j = m !! j;
   lookup_fmap {A B} (f : A → B) (m : M A) i : (f <$> m) !! i = f <$> m !! i;
-  map_to_list_nodup {A} (m : M A) : NoDup (map_to_list m);
+  NoDup_map_to_list {A} (m : M A) : NoDup (map_to_list m);
   elem_of_map_to_list {A} (m : M A) i x :
     (i,x) ∈ map_to_list m ↔ m !! i = Some x;
   lookup_omap {A B} (f : A → option B) m i : omap f m !! i = m !! i ≫= f;
@@ -58,8 +58,8 @@ Instance map_delete `{PartialAlter K A M} : Delete K M :=
 Instance map_singleton `{PartialAlter K A M, Empty M} :
   Singleton (K * A) M := λ p, <[p.1:=p.2]> ∅.
 
-Definition map_of_list `{Insert K A M} `{Empty M}
-  (l : list (K * A)) : M := insert_list l ∅.
+Definition map_of_list `{Insert K A M} `{Empty M} : list (K * A) → M :=
+  fold_right (λ p, <[p.1:=p.2]>) ∅.
 
 Instance map_union_with `{Merge M} {A} : UnionWith A (M A) :=
   λ f, merge (union_with f).
@@ -81,11 +81,7 @@ Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B}
   | None, Some y => Q y
   | None, None => True
   end.
-(*
-Definition map_intersection_Forall `{Lookup K A M}
-    (R : relation A) : relation M := λ m1 m2,
-  ∀ i x1 x2, m1 !! i = Some x1 → m2 !! i = Some x2 → R x1 x2.
-*)
+
 Instance map_disjoint `{∀ A, Lookup K A (M A)} {A} : Disjoint (M A) :=
   map_Forall2 (λ _ _, False) (λ _, True) (λ _, True).
 Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
@@ -396,7 +392,7 @@ Lemma lookup_singleton {A} i (x : A) : {[i, x]} !! i = Some x.
 Proof. by rewrite lookup_singleton_Some. Qed.
 Lemma lookup_singleton_ne {A} i j (x : A) : i ≠ j → {[i, x]} !! j = None.
 Proof. by rewrite lookup_singleton_None. Qed.
-Lemma singleton_ne_empty {A} i (x : A) : {[i,x]} ≠ ∅.
+Lemma map_non_empty_singleton {A} i (x : A) : {[i,x]} ≠ ∅.
 Proof.
   intros Hix. apply (f_equal (!! i)) in Hix.
   by rewrite lookup_empty, lookup_singleton in Hix.
@@ -429,8 +425,8 @@ Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
 Lemma map_to_list_unique {A} (m : M A) i x y :
   (i,x) ∈ map_to_list m → (i,y) ∈ map_to_list m → x = y.
 Proof. rewrite !elem_of_map_to_list. congruence. Qed.
-Lemma map_to_list_key_nodup {A} (m : M A) : NoDup (fst <$> map_to_list m).
-Proof. eauto using NoDup_fmap_fst, map_to_list_unique, map_to_list_nodup. Qed.
+Lemma NoDup_fst_map_to_list {A} (m : M A) : NoDup (fst <$> map_to_list m).
+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.
@@ -477,23 +473,23 @@ Lemma map_of_list_inj {A} (l1 l2 : list (K * A)) :
   NoDup (fst <$> l1) → NoDup (fst <$> l2) →
   map_of_list l1 = map_of_list l2 → l1 ≡ₚ l2.
 Proof.
-  intros ?? Hl1l2. apply NoDup_Permutation; auto using (fmap_nodup_1 fst).
+  intros ?? Hl1l2. apply NoDup_Permutation; auto using (NoDup_fmap_1 fst).
   intros [i x]. by rewrite !elem_of_map_of_list, Hl1l2.
 Qed.
 Lemma map_of_to_list {A} (m : M A) : map_of_list (map_to_list m) = m.
 Proof.
   apply map_eq. intros i. apply option_eq. intros x.
   by rewrite <-elem_of_map_of_list, elem_of_map_to_list
-    by auto using map_to_list_key_nodup.
+    by auto using NoDup_fst_map_to_list.
 Qed.
 Lemma map_to_of_list {A} (l : list (K * A)) :
   NoDup (fst <$> l) → map_to_list (map_of_list l) ≡ₚ l.
-Proof. auto using map_of_list_inj, map_to_list_key_nodup, map_of_to_list. Qed.
+Proof. auto using map_of_list_inj, NoDup_fst_map_to_list, map_of_to_list. Qed.
 Lemma map_to_list_inj {A} (m1 m2 : M A) :
   map_to_list m1 ≡ₚ map_to_list m2 → m1 = m2.
 Proof.
   intros. rewrite <-(map_of_to_list m1), <-(map_of_to_list m2).
-  auto using map_of_list_proper, map_to_list_key_nodup.
+  auto using map_of_list_proper, NoDup_fst_map_to_list.
 Qed.
 Lemma map_to_list_empty {A} : map_to_list ∅ = @nil (K * A).
 Proof.
@@ -504,8 +500,8 @@ 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.
-  * apply map_to_list_key_nodup.
-  * constructor; auto using map_to_list_key_nodup.
+  * apply NoDup_fst_map_to_list.
+  * constructor; auto using NoDup_fst_map_to_list.
     rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
     rewrite elem_of_map_to_list in Hlookup. congruence.
   * by rewrite !map_of_to_list.
@@ -524,11 +520,17 @@ Lemma map_to_list_insert_inv {A} (m : M A) l i x :
 Proof.
   intros Hperm. apply map_to_list_inj.
   assert (NoDup (fst <$> (i, x) :: l)) as Hnodup.
-  { rewrite <-Hperm. auto using map_to_list_key_nodup. }
+  { rewrite <-Hperm. auto using NoDup_fst_map_to_list. }
   simpl in Hnodup. 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.
+Lemma map_choose {A} (m : M A) : m ≠ ∅ → ∃ i x, m !! i = Some x.
+Proof.
+  intros Hemp. destruct (map_to_list m) as [|[i x] l] eqn:Hm.
+  { destruct Hemp; eauto using map_to_list_empty_inv. }
+  exists i x. rewrite <-elem_of_map_to_list, Hm. by left.
+Qed.
 
 (** * Induction principles *)
 Lemma map_ind {A} (P : M A → Prop) :
@@ -536,7 +538,7 @@ Lemma map_ind {A} (P : M A → Prop) :
 Proof.
   intros ? Hins. cut (∀ l, NoDup (fst <$> l) → ∀ m, map_to_list m ≡ₚ l → P m).
   { intros help m.
-    apply (help (map_to_list m)); auto using map_to_list_key_nodup. }
+    apply (help (map_to_list m)); auto using NoDup_fst_map_to_list. }
   induction l as [|[i x] l IH]; intros Hnodup m Hml.
   { apply map_to_list_empty_inv_alt in Hml. by subst. }
   inversion_clear Hnodup.
@@ -745,7 +747,7 @@ Lemma map_not_disjoint {A} (m1 m2 : M A) :
 Proof.
   unfold disjoint, map_disjoint. rewrite map_not_Forall2 by solve_decision.
   split; [|naive_solver].
-  * intros [i[(x&y&?&?&?)|[(x&?&?&[])|(y&?&?&[])]]]; naive_solver.
+  intros [i[(x&y&?&?&?)|[(x&?&?&[])|(y&?&?&[])]]]; naive_solver.
 Qed.
 Global Instance: Symmetric (@disjoint (M A) _).
 Proof. intros A m1 m2. rewrite !map_disjoint_spec. naive_solver. Qed.
@@ -801,6 +803,15 @@ Context {A} (f : A → A → option A).
 Lemma lookup_union_with m1 m2 i :
   union_with f m1 m2 !! i = union_with f (m1 !! i) (m2 !! i).
 Proof. by rewrite <-(lookup_merge _). Qed.
+Lemma lookup_union_with_Some m1 m2 i z :
+  union_with f m1 m2 !! i = Some z ↔
+    (m1 !! i = Some z ∧ m2 !! i = None) ∨
+    (m1 !! i = None ∧ m2 !! i = Some z) ∨
+    (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
+Proof.
+  rewrite lookup_union_with.
+  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
+Qed.
 Global Instance: LeftId (@eq (M A)) ∅ (union_with f).
 Proof. unfold union_with, map_union_with. apply _. Qed.
 Global Instance: RightId (@eq (M A)) ∅ (union_with f).
@@ -847,9 +858,9 @@ Qed.
 Lemma delete_union_with m1 m2 i :
   delete i (union_with f m1 m2) = union_with f (delete i m1) (delete i m2).
 Proof. by apply (partial_alter_merge _). Qed.
-Lemma delete_list_union_with (m1 m2 : M A) is :
-  delete_list is (union_with f m1 m2) =
-    union_with f (delete_list is m1) (delete_list is m2).
+Lemma foldr_delete_union_with (m1 m2 : M A) is :
+  foldr delete (union_with f m1 m2) is =
+    union_with f (foldr delete m1 is) (foldr delete m2 is).
 Proof. induction is; simpl. done. by rewrite IHis, delete_union_with. Qed.
 Lemma insert_union_with m1 m2 i x :
   (∀ x, f x x = Some x) →
@@ -880,7 +891,6 @@ Proof.
 Qed.
 Global Instance: Idempotent (@eq (M A)) (∪).
 Proof. intros A ?. by apply union_with_idempotent. Qed.
-
 Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x :
   (m1 ∪ m2) !! i = Some x ↔
     m1 !! i = Some x ∨ (m1 !! i = None ∧ m2 !! i = Some x).
@@ -894,6 +904,13 @@ Proof.
   unfold union, map_union, union_with, map_union_with. rewrite (lookup_merge _).
   destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
 Qed.
+Lemma map_positive_l {A} (m1 m2 : M A) : m1 ∪ m2 = ∅ → m1 = ∅.
+Proof.
+  intros Hm. apply map_empty. intros i. apply (f_equal (!! i)) in Hm.
+  rewrite lookup_empty, lookup_union_None in Hm; tauto.
+Qed.
+Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 ≠ ∅ → m1 ∪ m2 ≠ ∅.
+Proof. eauto using map_positive_l. Qed.
 Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
   m1 ⊥ m2 → (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x.
 Proof.
@@ -1028,11 +1045,11 @@ Proof.
   rewrite (map_union_commutative m1); [done |].
   by apply map_disjoint_singleton_r.
 Qed.
-Lemma insert_list_union {A} (m : M A) l : insert_list l m = map_of_list l ∪ m.
+Lemma foldr_insert_union {A} (m : M A) l :
+  foldr (λ p, <[p.1:=p.2]>) m l = map_of_list l ∪ m.
 Proof.
-  induction l; simpl.
-  * by rewrite (left_id_L _ _).
-  * by rewrite IHl, insert_union_l.
+  induction l as [|i l IH]; simpl; [by rewrite (left_id_L _ _)|].
+  by rewrite IH, insert_union_l.
 Qed.
 Lemma delete_union {A} (m1 m2 : M A) i :
   delete i (m1 ∪ m2) = delete i m1 ∪ delete i m2.
@@ -1066,47 +1083,38 @@ Proof.
   * apply map_union_preserving_l; auto.
 Qed.
 
-(** ** Properties of the [intersection] operation *)
-Lemma lookup_intersection_Some {A} (m1 m2 : M A) i x :
-  (m1 ∩ m2) !! i = Some x ↔ m1 !! i = Some x ∧ is_Some (m2 !! i).
-Proof.
-  unfold intersection, map_intersection, intersection_with,
-    map_intersection_with. rewrite (lookup_merge _).
-  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
-Qed.
-
-(** ** Properties of the [delete_list] function *)
-Lemma lookup_delete_list {A} (m : M A) is j :
-  j ∈ is → delete_list is m !! j = None.
+(** ** Properties of the folding the [delete] function *)
+Lemma lookup_foldr_delete {A} (m : M A) is j :
+  j ∈ is → foldr delete m is !! j = None.
 Proof.
   induction 1 as [|i j is]; simpl; [by rewrite lookup_delete|].
   by destruct (decide (i = j)) as [->|?];
     rewrite ?lookup_delete, ?lookup_delete_ne by done.
 Qed.
-Lemma lookup_delete_list_not_elem_of {A} (m : M A) is j :
-  j ∉ is → delete_list is m !! j = m !! j.
+Lemma lookup_foldr_delete_not_elem_of {A} (m : M A) is j :
+  j ∉ is → foldr delete m is !! j = m !! j.
 Proof.
   induction is; simpl; [done |]. rewrite elem_of_cons; intros.
   rewrite lookup_delete_ne; intuition.
 Qed.
-Lemma delete_list_notin {A} (m : M A) is :
-  Forall (λ i, m !! i = None) is → delete_list is m = m.
+Lemma foldr_delete_notin {A} (m : M A) is :
+  Forall (λ i, m !! i = None) is → foldr delete m is = m.
 Proof. induction 1; simpl; [done |]. rewrite delete_notin; congruence. Qed.
-Lemma delete_list_insert_ne {A} (m : M A) is j x :
-  j ∉ is → delete_list is (<[j:=x]>m) = <[j:=x]>(delete_list is m).
+Lemma foldr_delete_insert_ne {A} (m : M A) is j x :
+  j ∉ is → foldr delete (<[j:=x]>m) is = <[j:=x]>(foldr delete m is).
 Proof.
   induction is; simpl; [done |]. rewrite elem_of_cons. intros.
   rewrite IHis, delete_insert_ne; intuition.
 Qed.
-Lemma map_disjoint_delete_list_l {A} (m1 m2 : M A) is :
-  m1 ⊥ m2 → delete_list is m1 ⊥ m2.
+Lemma map_disjoint_foldr_delete_l {A} (m1 m2 : M A) is :
+  m1 ⊥ m2 → foldr delete m1 is ⊥ m2.
 Proof. induction is; simpl; auto using map_disjoint_delete_l. Qed.
-Lemma map_disjoint_delete_list_r {A} (m1 m2 : M A) is :
-  m1 ⊥ m2 → m1 ⊥ delete_list is m2.
+Lemma map_disjoint_foldr_delete_r {A} (m1 m2 : M A) is :
+  m1 ⊥ m2 → m1 ⊥ foldr delete m2 is.
 Proof. induction is; simpl; auto using map_disjoint_delete_r. Qed.
-Lemma delete_list_union {A} (m1 m2 : M A) is :
-  delete_list is (m1 ∪ m2) = delete_list is m1 ∪ delete_list is m2.
-Proof. apply delete_list_union_with. Qed.
+Lemma foldr_delete_union {A} (m1 m2 : M A) is :
+  foldr delete (m1 ∪ m2) is = foldr delete m1 is ∪ foldr delete m2 is.
+Proof. apply foldr_delete_union_with. Qed.
 
 (** ** Properties on disjointness of conversion to lists *)
 Lemma map_disjoint_of_list_l {A} (m : M A) ixs :
@@ -1144,9 +1152,8 @@ Proof. intro. by rewrite map_disjoint_of_list_zip_r. Qed.
 Lemma union_delete_vec {A n} (ms : vec (M A) n) (i : fin n) :
   ⊥ ms → ms !!! i ∪ ⋃ delete (fin_to_nat i) (vec_to_list ms) = ⋃ ms.
 Proof.
-  induction ms as [|m ? ms]; inversion_clear 1;
-    inv_fin i; simpl; [done | intros i].
-  rewrite (map_union_commutative m), (associative_L (∪)), IHms.
+  induction ms as [|m ? ms IH]; inversion_clear 1; inv_fin i; simpl; auto.
+  intros i. rewrite (map_union_commutative m), (associative_L (∪)), IH.
   * by rewrite map_union_commutative.
   * done.
   * apply map_disjoint_weaken_r with (⋃ ms); [done |].
@@ -1161,10 +1168,44 @@ Proof.
   rewrite IH, !(associative_L (∪)), (map_union_commutative m); intuition.
 Qed.
 
+(** ** Properties of the [intersection_with] operation *)
+Lemma lookup_intersection_with {A} (f : A → A → option A) m1 m2 i :
+  intersection_with f m1 m2 !! i = intersection_with f (m1 !! i) (m2 !! i).
+Proof. by rewrite <-(lookup_merge _). Qed.
+Lemma lookup_intersection_with_Some {A} (f : A → A → option A) m1 m2 i z :
+  intersection_with f m1 m2 !! i = Some z ↔
+    (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
+Proof.
+  rewrite lookup_intersection_with.
+  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
+Qed.
+
+(** ** Properties of the [intersection] operation *)
+Lemma lookup_intersection_Some {A} (m1 m2 : M A) i x :
+  (m1 ∩ m2) !! i = Some x ↔ m1 !! i = Some x ∧ is_Some (m2 !! i).
+Proof.
+  unfold intersection, map_intersection. rewrite lookup_intersection_with.
+  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
+Qed.
+Lemma lookup_intersection_None {A} (m1 m2 : M A) i :
+  (m1 ∩ m2) !! i = None ↔ m1 !! i = None ∨ m2 !! i = None.
+Proof.
+  unfold intersection, map_intersection. rewrite lookup_intersection_with.
+  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
+Qed.
+
 (** ** Properties of the [difference_with] operation *)
 Lemma lookup_difference_with {A} (f : A → A → option A) m1 m2 i :
   difference_with f m1 m2 !! i = difference_with f (m1 !! i) (m2 !! i).
 Proof. by rewrite <-lookup_merge by done. Qed.
+Lemma lookup_difference_with_Some {A} (f : A → A → option A) m1 m2 i z :
+  difference_with f m1 m2 !! i = Some z ↔
+    (m1 !! i = Some z ∧ m2 !! i = None) ∨
+    (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
+Proof.
+  rewrite lookup_difference_with.
+  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
+Qed.
 
 (** ** Properties of the [difference] operation *)
 Lemma lookup_difference_Some {A} (m1 m2 : M A) i x :
@@ -1173,6 +1214,12 @@ Proof.
   unfold difference, map_difference; rewrite lookup_difference_with.
   destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
 Qed.
+Lemma lookup_difference_None {A} (m1 m2 : M A) i :
+  (m1 ∖ m2) !! i = None ↔ m1 !! i = None ∨ is_Some (m2 !! i).
+Proof.
+  unfold difference, map_difference; rewrite lookup_difference_with.
+  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
+Qed.
 Lemma map_disjoint_difference_l {A} (m1 m2 : M A) : m1 ⊆ m2 → m2 ∖ m1 ⊥ m1.
 Proof.
   intros Hm i; specialize (Hm i).
@@ -1249,10 +1296,10 @@ Hint Extern 2 (_ ⊥ map_of_list _) =>
   apply map_disjoint_of_list_zip_r_2 : mem_disjoint.
 Hint Extern 2 (⋃ _ ⊥ _) => apply map_disjoint_union_list_l_2 : mem_disjoint.
 Hint Extern 2 (_ ⊥ ⋃ _) => apply map_disjoint_union_list_r_2 : mem_disjoint.
-Hint Extern 2 (delete_list _ _ ⊥ _) =>
-  apply map_disjoint_delete_list_l : map_disjoint.
-Hint Extern 2 (_ ⊥ delete_list _ _) =>
-  apply map_disjoint_delete_list_r : map_disjoint.
+Hint Extern 2 (foldr delete _ _ ⊥ _) =>
+  apply map_disjoint_foldr_delete_l : map_disjoint.
+Hint Extern 2 (_ ⊥ foldr delete _ _) =>
+  apply map_disjoint_foldr_delete_r : map_disjoint.
 
 (** The tactic [simpl_map by tac] simplifies occurrences of finite map look
 ups. It uses [tac] to discharge generated inequalities. Look ups in unions do
@@ -1323,8 +1370,8 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
     apply map_union_cancel_l in H; [|by tac|by tac]
   | H : _ ∪ ?m = _ ∪ ?m |- _ =>
     apply map_union_cancel_r in H; [|by tac|by tac]
-  | H : {[?i,?x]} = ∅ |- _ => by destruct (singleton_ne_empty i x)
-  | H : ∅ = {[?i,?x]} |- _ => by destruct (singleton_ne_empty i x)
+  | H : {[?i,?x]} = ∅ |- _ => by destruct (map_non_empty_singleton i x)
+  | 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).
diff --git a/theories/finite.v b/theories/finite.v
index 4bcaa09f48aa759d0094df6a02a38fb4ae3ca7d7..2dc8b648cec2ac81f472da46d546818773cf8bde 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -5,11 +5,11 @@ Obligation Tactic := idtac.
 
 Class Finite A `{∀ x y : A, Decision (x = y)} := {
   enum : list A;
-  enum_nodup : NoDup enum;
+  NoDup_enum : NoDup enum;
   elem_of_enum x : x ∈ enum
 }.
 Arguments enum _ {_ _} : clear implicits.
-Arguments enum_nodup _ {_ _} : clear implicits.
+Arguments NoDup_enum _ {_ _} : clear implicits.
 Definition card A `{Finite A} := length (enum A).
 Program Instance finite_countable `{Finite A} : Countable A := {|
   encode := λ x, Pos.of_nat $ S $ from_option 0 $ list_find (x =) (enum A);
@@ -72,7 +72,7 @@ Qed.
 Lemma finite_injective_contains `{finA: Finite A} `{finB: Finite B} (f: A → B)
   `{!Injective (=) (=) f} : f <$> enum A `contains` enum B.
 Proof.
-  intros. destruct finA, finB. apply NoDup_contains; auto using fmap_nodup_2.
+  intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2.
 Qed.
 Lemma finite_injective_Permutation `{Finite A} `{Finite B} (f : A → B)
   `{!Injective (=) (=) f} : card A = card B → f <$> enum A ≡ₚ enum B.
@@ -181,7 +181,7 @@ Section bijective_finite.
   Context `{!Injective (=) (=) f} `{!Cancel (=) f g}.
 
   Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
-  Next Obligation. apply (fmap_nodup _), enum_nodup. Qed.
+  Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
   Next Obligation.
     intros y. rewrite elem_of_list_fmap. eauto using elem_of_enum.
   Qed.
@@ -192,7 +192,7 @@ Program Instance option_finite `{Finite A} : Finite (option A) :=
 Next Obligation.
   constructor.
   * rewrite elem_of_list_fmap. by intros (?&?&?).
-  * apply (fmap_nodup _); auto using enum_nodup.
+  * apply (NoDup_fmap_2 _); auto using NoDup_enum.
 Qed.
 Next Obligation.
   intros ??? [x|]; [right|left]; auto.
@@ -219,9 +219,9 @@ Program Instance sum_finite `{Finite A} `{Finite B} : Finite (A + B)%type :=
   {| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
 Next Obligation.
   intros. apply NoDup_app; split_ands.
-  * apply (fmap_nodup _). by apply enum_nodup.
+  * apply (NoDup_fmap_2 _). by apply NoDup_enum.
   * intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
-  * apply (fmap_nodup _). by apply enum_nodup.
+  * apply (NoDup_fmap_2 _). by apply NoDup_enum.
 Qed.
 Next Obligation.
   intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
@@ -233,10 +233,10 @@ Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
 Program Instance prod_finite `{Finite A} `{Finite B} : Finite (A * B)%type :=
   {| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}.
 Next Obligation.
-  intros ??????. induction (enum_nodup A) as [|x xs Hx Hxs IH]; simpl.
+  intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
   { constructor. }
   apply NoDup_app; split_ands.
-  * apply (fmap_nodup _). by apply enum_nodup.
+  * by apply (NoDup_fmap_2 _), NoDup_enum.
   * intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_equality.
     clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
     { rewrite elem_of_nil. tauto. }
@@ -268,9 +268,9 @@ Program Instance list_finite `{Finite A} n : Finite { l | length l = n } :=
 Next Obligation.
   intros ????. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
   revert IH. generalize (list_enum (enum A) n). intros l Hl.
-  induction (enum_nodup A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
+  induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
   apply NoDup_app; split_ands.
-  * by apply (fmap_nodup _).
+  * by apply (NoDup_fmap_2 _).
   * intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
     intros ([k2 Hk2]&?&?) Hxk2; simplify_equality. destruct Hx. revert Hxk2.
     induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
diff --git a/theories/list.v b/theories/list.v
index 17878a5d873440c8e0937a9dbd106904755e5923..22ae4efcc7f262e41d7d00909f15559c16de379f 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -275,6 +275,7 @@ Section list_set.
       if decide_rel (∈) x k
       then list_difference l k else x :: list_difference l k
     end.
+  Definition list_union (l k : list A) : list A := list_difference l k ++ k.
   Fixpoint list_intersection (l k : list A) : list A :=
     match l with
     | [] => []
@@ -495,6 +496,8 @@ Lemma elem_of_nil x : x ∈ [] ↔ False.
 Proof. intuition. by destruct (not_elem_of_nil x). Qed.
 Lemma elem_of_nil_inv l : (∀ x, x ∉ l) → l = [].
 Proof. destruct l. done. by edestruct 1; constructor. Qed.
+Lemma elem_of_not_nil x l : x ∈ l → l ≠ [].
+Proof. intros ? ->. by apply (elem_of_nil x). Qed.
 Lemma elem_of_cons l x y : x ∈ y :: l ↔ x = y ∨ x ∈ l.
 Proof. split; [inversion 1; subst|intros [->|?]]; constructor (done). Qed.
 Lemma not_elem_of_cons l x y : x ∉ y :: l ↔ x ≠ y ∧ x ∉ l.
@@ -528,57 +531,6 @@ Qed.
 Lemma elem_of_list_lookup l x : x ∈ l ↔ ∃ i, l !! i = Some x.
 Proof. firstorder eauto using elem_of_list_lookup_1, elem_of_list_lookup_2. Qed.
 
-(** ** Set operations on lists *)
-Section list_set.
-  Context {dec : ∀ x y, Decision (x = y)}.
-  Lemma elem_of_list_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k.
-  Proof.
-    split; induction l; simpl; try case_decide;
-      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
-  Qed.
-  Lemma list_difference_nodup l k : NoDup l → NoDup (list_difference l k).
-  Proof.
-    induction 1; simpl; try case_decide.
-    * constructor.
-    * done.
-    * constructor. rewrite elem_of_list_difference; intuition. done.
-  Qed.
-  Lemma elem_of_list_intersection l k x :
-    x ∈ list_intersection l k ↔ x ∈ l ∧ x ∈ k.
-  Proof.
-    split; induction l; simpl; repeat case_decide;
-      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
-  Qed.
-  Lemma list_intersection_nodup l k : NoDup l → NoDup (list_intersection l k).
-  Proof.
-    induction 1; simpl; try case_decide.
-    * constructor.
-    * constructor. rewrite elem_of_list_intersection; intuition. done.
-    * done.
-  Qed.
-  Lemma elem_of_list_intersection_with f l k x :
-    x ∈ list_intersection_with f l k ↔ ∃ x1 x2,
-      x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x.
-  Proof.
-    split.
-    * induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
-      intros Hx. setoid_rewrite elem_of_cons.
-      cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x)
-        ∨ x ∈ list_intersection_with f l k); [naive_solver|].
-      clear IH. revert Hx. generalize (list_intersection_with f l k).
-      induction k; simpl; [by auto|].
-      case_match; setoid_rewrite elem_of_cons; naive_solver.
-    * intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl.
-      + generalize (list_intersection_with f l k).
-        induction Hx2; simpl; [by rewrite Hx; left |].
-        case_match; simpl; try setoid_rewrite elem_of_cons; auto.
-      + generalize (IH Hx). clear Hx IH Hx2.
-        generalize (list_intersection_with f l k).
-        induction k; simpl; intros; [done|].
-        case_match; simpl; rewrite ?elem_of_cons; auto.
-  Qed.
-End list_set.
-
 (** ** Properties of the [NoDup] predicate *)
 Lemma NoDup_nil : NoDup (@nil A) ↔ True.
 Proof. split; constructor. Qed.
@@ -644,13 +596,76 @@ Section no_dup_dec.
     split; induction l; simpl; repeat case_decide;
       rewrite ?elem_of_cons; intuition (simplify_equality; auto).
   Qed.
-  Lemma remove_dups_nodup l : NoDup (remove_dups l).
+  Lemma NoDup_remove_dups l : NoDup (remove_dups l).
   Proof.
     induction l; simpl; repeat case_decide; try constructor; auto.
     by rewrite elem_of_remove_dups.
   Qed.
 End no_dup_dec.
 
+(** ** Set operations on lists *)
+Section list_set.
+  Context {dec : ∀ x y, Decision (x = y)}.
+  Lemma elem_of_list_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k.
+  Proof.
+    split; induction l; simpl; try case_decide;
+      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
+  Qed.
+  Lemma NoDup_list_difference l k : NoDup l → NoDup (list_difference l k).
+  Proof.
+    induction 1; simpl; try case_decide.
+    * constructor.
+    * done.
+    * constructor. rewrite elem_of_list_difference; intuition. done.
+  Qed.
+  Lemma elem_of_list_union l k x : x ∈ list_union l k ↔ x ∈ l ∨ x ∈ k.
+  Proof.
+    unfold list_union. rewrite elem_of_app, elem_of_list_difference.
+    intuition. case (decide (x ∈ k)); intuition.
+  Qed.
+  Lemma NoDup_list_union l k : NoDup l → NoDup k → NoDup (list_union l k).
+  Proof.
+    intros. apply NoDup_app. repeat split.
+    * by apply NoDup_list_difference.
+    * intro. rewrite elem_of_list_difference. intuition.
+    * done.
+  Qed.
+  Lemma elem_of_list_intersection l k x :
+    x ∈ list_intersection l k ↔ x ∈ l ∧ x ∈ k.
+  Proof.
+    split; induction l; simpl; repeat case_decide;
+      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
+  Qed.
+  Lemma NoDup_list_intersection l k : NoDup l → NoDup (list_intersection l k).
+  Proof.
+    induction 1; simpl; try case_decide.
+    * constructor.
+    * constructor. rewrite elem_of_list_intersection; intuition. done.
+    * done.
+  Qed.
+  Lemma elem_of_list_intersection_with f l k x :
+    x ∈ list_intersection_with f l k ↔ ∃ x1 x2,
+      x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x.
+  Proof.
+    split.
+    * induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
+      intros Hx. setoid_rewrite elem_of_cons.
+      cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x)
+        ∨ x ∈ list_intersection_with f l k); [naive_solver|].
+      clear IH. revert Hx. generalize (list_intersection_with f l k).
+      induction k; simpl; [by auto|].
+      case_match; setoid_rewrite elem_of_cons; naive_solver.
+    * intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl.
+      + generalize (list_intersection_with f l k).
+        induction Hx2; simpl; [by rewrite Hx; left |].
+        case_match; simpl; try setoid_rewrite elem_of_cons; auto.
+      + generalize (IH Hx). clear Hx IH Hx2.
+        generalize (list_intersection_with f l k).
+        induction k; simpl; intros; [done|].
+        case_match; simpl; rewrite ?elem_of_cons; auto.
+  Qed.
+End list_set.
+
 (** ** Properties of the [filter] function *)
 Section filter.
   Context (P : A → Prop) `{∀ x, Decision (P x)}.
@@ -659,7 +674,7 @@ Section filter.
     unfold filter. induction l; simpl; repeat case_decide;
        rewrite ?elem_of_nil, ?elem_of_cons; naive_solver.
   Qed.
-  Lemma filter_nodup l : NoDup l → NoDup (filter P l).
+  Lemma NoDup_filter l : NoDup l → NoDup (filter P l).
   Proof.
     unfold filter. induction 1; simpl; repeat case_decide;
       rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
@@ -726,6 +741,10 @@ Qed.
 (** ** Properties of the [last] function *)
 Lemma last_snoc x l : last (l ++ [x]) = Some x.
 Proof. induction l as [|? []]; simpl; auto. Qed.
+Lemma last_reverse l : last (reverse l) = head l.
+Proof. by destruct l as [|x l]; rewrite ?reverse_cons, ?last_snoc. Qed.
+Lemma head_reverse l : head (reverse l) = last l.
+Proof. by rewrite <-last_reverse, reverse_involutive. Qed.
 
 (** ** Properties of the [take] function *)
 Definition take_drop i l : take i l ++ drop i l = l := firstn_skipn i l.
@@ -757,11 +776,9 @@ Lemma take_length_le l n : n ≤ length l → length (take n l) = n.
 Proof. rewrite take_length. apply Min.min_l. Qed.
 Lemma take_length_ge l n : length l ≤ n → length (take n l) = length l.
 Proof. rewrite take_length. apply Min.min_r. Qed.
-Lemma take_drop_commute l n m :
-  n ≤ m → take (m - n) (drop n l) = drop n (take m l).
+Lemma take_drop_commute l n m : take n (drop m l) = drop m (take (m + n) l).
 Proof.
-  revert n m. induction l; intros [|?] [|?] ?;
-    simpl; auto using take_nil with lia.
+  revert n m. induction l; intros [|?][|?]; simpl; auto using take_nil with lia.
 Qed.
 Lemma lookup_take l n i : i < n → take n l !! i = l !! i.
 Proof. revert n i. induction l; intros [|n] [|i] ?; simpl; auto with lia. Qed.
@@ -781,6 +798,8 @@ Proof.
 Qed.
 
 (** ** Properties of the [drop] function *)
+Lemma drop_0 l : drop 0 l = l.
+Proof. done. Qed.
 Lemma drop_nil n : drop n (@nil A) = [].
 Proof. by destruct n. Qed.
 Lemma drop_length l n : length (drop n l) = length l - n.
@@ -863,6 +882,8 @@ Proof.
   rewrite reverse_length, replicate_length. split; auto.
   intros y. rewrite elem_of_reverse. by apply elem_of_replicate_inv.
 Qed.
+Lemma replicate_false βs n : length βs = n → replicate n false =.>* βs.
+Proof. intros <-. by induction βs; simpl; constructor. Qed.
 
 (** ** Properties of the [resize] function *)
 Lemma resize_spec l n x : resize n x l = take n l ++ replicate (n - length l) x.
@@ -1051,8 +1072,8 @@ Proof.
   unfold sublist_lookup; intros; simplify_option_equality;
     repeat match goal with
     | H : _ ≤ length _ |- _ => rewrite take_length, drop_length in H
-    end; rewrite <-?take_drop_commute, ?drop_drop, ?take_take, ?Min.min_l by lia;
-    auto with lia.
+    end; rewrite ?take_drop_commute, ?drop_drop, ?take_take,
+      ?Min.min_l, Nat.add_assoc by lia; auto with lia.
 Qed.
 Lemma sublist_alter_length f l i n k :
   sublist_lookup i n l = Some k → length (f k) = n →
@@ -1122,6 +1143,12 @@ Proof.
   unfold sublist_lookup; rewrite mask_length; simplify_option_equality; auto.
   by rewrite drop_mask, take_mask.
 Qed.
+Lemma mask_mask f g βs1 βs2 l :
+  (∀ x, f (g x) = f x) → βs1 =.>* βs2 →
+  mask f βs2 (mask g βs1 l) = mask f βs2 l.
+Proof.
+  intros ? Hβs. revert l. by induction Hβs as [|[] []]; intros [|??]; f_equal'.
+Qed.
 
 (** ** Properties of the [seq] function *)
 Lemma fmap_seq j n : S <$> seq j n = seq (S j) n.
@@ -1525,24 +1552,22 @@ Lemma sublist_drop l i : drop i l `sublist` l.
 Proof. rewrite <-(take_drop i l) at 2. by apply sublist_inserts_l. Qed.
 Lemma sublist_delete l i : delete i l `sublist` l.
 Proof. revert i. by induction l; intros [|?]; simpl; constructor. Qed.
-Lemma sublist_delete_list l is : delete_list is l `sublist` l.
+Lemma sublist_foldr_delete l is : foldr delete l is `sublist` l.
 Proof.
   induction is as [|i is IH]; simpl; [done |].
-  transitivity (delete_list is l); auto using sublist_delete.
+  transitivity (foldr delete l is); auto using sublist_delete.
 Qed.
-Lemma sublist_alt l1 l2 : l1 `sublist` l2 ↔ ∃ is, l1 = delete_list is l2.
+Lemma sublist_alt l1 l2 : l1 `sublist` l2 ↔ ∃ is, l1 = foldr delete l2 is.
 Proof.
-  split.
-  * intros Hl12. cut (∀ k, ∃ is, k ++ l1 = delete_list is (k ++ l2)).
-    { intros help. apply (help []). }
-    induction Hl12 as [|x l1 l2 _ IH|x l1 l2 _ IH]; intros k.
-    + by eexists [].
-    + destruct (IH (k ++ [x])) as [is His]. exists is.
-      by rewrite <-!(associative_L (++)) in His.
-    + destruct (IH k) as [is His]. exists (is ++ [length k]).
-      unfold delete_list. rewrite fold_right_app. simpl.
-      by rewrite delete_middle.
-  * intros [is ->]. apply sublist_delete_list.
+  split; [|intros [is ->]; apply sublist_foldr_delete].
+  intros Hl12. cut (∀ k, ∃ is, k ++ l1 = foldr delete (k ++ l2) is).
+  { intros help. apply (help []). }
+  induction Hl12 as [|x l1 l2 _ IH|x l1 l2 _ IH]; intros k.
+  * by eexists [].
+  * destruct (IH (k ++ [x])) as [is His]. exists is.
+    by rewrite <-!(associative_L (++)) in His.
+  * destruct (IH k) as [is His]. exists (is ++ [length k]).
+    rewrite fold_right_app. simpl. by rewrite delete_middle.
 Qed.
 Lemma Permutation_sublist l1 l2 l3 :
   l1 ≡ₚ l2 → l2 `sublist` l3 → ∃ l4, l1 `sublist` l4 ∧ l4 ≡ₚ l3.
@@ -1640,8 +1665,8 @@ Lemma contains_drop l i : drop i l `contains` l.
 Proof. auto using sublist_drop, sublist_contains. Qed.
 Lemma contains_delete l i : delete i l `contains` l.
 Proof. auto using sublist_delete, sublist_contains. Qed.
-Lemma contains_delete_list l is : delete_list is l `sublist` l.
-Proof. auto using sublist_delete_list, sublist_contains. Qed.
+Lemma contains_foldr_delete l is : foldr delete l is `sublist` l.
+Proof. auto using sublist_foldr_delete, sublist_contains. Qed.
 Lemma contains_sublist_l l1 l3 :
   l1 `contains` l3 ↔ ∃ l2, l1 `sublist` l2 ∧ l2 ≡ₚ l3.
 Proof.
@@ -1975,6 +2000,22 @@ Section Forall_Exists.
   Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
   Proof. induction 1; inversion_clear 1; contradiction. Qed.
 
+  Lemma Forall_list_difference `{∀ x y : A, Decision (x = y)} l k :
+    Forall P l → Forall P (list_difference l k).
+  Proof.
+    rewrite !Forall_forall.
+    intros ? x; rewrite elem_of_list_difference; naive_solver.
+  Qed.
+  Lemma Forall_list_union `{∀ x y : A, Decision (x = y)} l k :
+    Forall P l → Forall P k → Forall P (list_union l k).
+  Proof. intros. apply Forall_app; auto using Forall_list_difference. Qed.
+  Lemma Forall_list_intersection `{∀ x y : A, Decision (x = y)} l k :
+    Forall P l → Forall P (list_intersection l k).
+  Proof.
+    rewrite !Forall_forall.
+    intros ? x; rewrite elem_of_list_intersection; naive_solver.
+  Qed.
+
   Context {dec : ∀ x, Decision (P x)}.
   Lemma not_Forall_Exists l : ¬Forall P l → Exists (not ∘ P) l.
   Proof. intro. destruct (Forall_Exists_dec dec l); intuition. Qed.
@@ -2388,18 +2429,18 @@ Section fmap.
   Proof.
     naive_solver eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
   Qed.
-  Lemma fmap_nodup_1 l : NoDup (f <$> l) → NoDup l.
+  Lemma NoDup_fmap_1 l : NoDup (f <$> l) → NoDup l.
   Proof.
     induction l; simpl; inversion_clear 1; constructor; auto.
     rewrite elem_of_list_fmap in *. naive_solver.
   Qed.
-  Lemma fmap_nodup_2 `{!Injective (=) (=) f} l : NoDup l → NoDup (f <$> l).
+  Lemma NoDup_fmap_2 `{!Injective (=) (=) f} l : NoDup l → NoDup (f <$> l).
   Proof.
     induction 1; simpl; constructor; trivial. rewrite elem_of_list_fmap.
     intros [y [Hxy ?]]. apply (injective f) in Hxy. by subst.
   Qed.
-  Lemma fmap_nodup `{!Injective (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
-  Proof. split; auto using fmap_nodup_1, fmap_nodup_2. Qed.
+  Lemma NoDup_fmap `{!Injective (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
+  Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
   Global Instance fmap_sublist: Proper (sublist ==> sublist) (fmap f).
   Proof. induction 1; simpl; econstructor; eauto. Qed.
   Global Instance fmap_contains: Proper (contains ==> contains) (fmap f).
@@ -2501,6 +2542,13 @@ Section bind.
       + destruct IH as [z [??]]. done. exists z. split; [done | by right].
     * intros [y [Hx Hy]]. induction Hy; simpl; 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.
+  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).
@@ -2529,12 +2577,6 @@ Section ret_join.
   Proof. by rewrite join_nil. Qed.
   Lemma join_nil_2 (ls : list (list A)) : Forall (= []) ls → mjoin ls = [].
   Proof. by rewrite join_nil. Qed.
-  Lemma join_length (ls : list (list A)) :
-    length (mjoin ls) = foldr (plus ∘ length) 0 ls.
-  Proof. by induction ls; simpl; rewrite ?app_length; f_equal. Qed.
-  Lemma join_length_same (ls : list (list A)) n :
-    Forall (λ l, length l = n) ls → length (mjoin ls) = length ls * n.
-  Proof. rewrite join_length. by induction 1; f_equal'. Qed.
   Lemma Forall_join (P : A → Prop) (ls: list (list A)) :
     Forall (Forall P) ls → Forall P (mjoin ls).
   Proof. induction 1; simpl; auto using Forall_app_2. Qed.
@@ -3059,7 +3101,8 @@ Ltac decompose_Forall_hyps := repeat
       apply Forall2_app_inv_r in H; destruct H as (l1&l2&?&?&->)
     | apply Forall2_app_inv_r in H; destruct H as (?&?&?&?&?) ]
   | H : Forall ?P ?l, H1 : ?l !! _ = Some ?x |- _ =>
-    unless (P x) by done;
+    (* to avoid some stupid loops, not fool proof *)
+    unless (P x) by auto using Forall_app_2, Forall_nil_2;
     let E := fresh in
     assert (P x) as E by (apply (Forall_lookup_1 P _ _ _ H H1)); lazy beta in E
   | H : Forall2 ?P ?l ?k |- _ =>
@@ -3094,8 +3137,9 @@ Ltac decompose_Forall := repeat
   | |- Forall _ _ => by apply Forall_true
   | |- Forall _ [] => constructor
   | |- Forall _ (_ :: _) => constructor
-  | |- Forall _ (_ ++ _) => apply Forall_app
+  | |- Forall _ (_ ++ _) => apply Forall_app_2
   | |- Forall _ (_ <$> _) => apply Forall_fmap
+  | |- Forall _ (_ ≫= _) => apply Forall_bind
   | |- Forall2 _ _ _ => apply Forall2_Forall
   | |- Forall2 _ [] [] => constructor
   | |- Forall2 _ (_ :: _) (_ :: _) => constructor
@@ -3106,6 +3150,7 @@ Ltac decompose_Forall := repeat
   | |- Forall2 _ _ (_ <$> _) => apply Forall2_fmap_r
   | _ => progress decompose_Forall_hyps
   | H : Forall _ (_ <$> _) |- _ => rewrite Forall_fmap in H
+  | H : Forall _ (_ ≫= _) |- _ => rewrite Forall_bind in H
   | |- Forall _ _ =>
     apply Forall_lookup_2; intros ???; progress decompose_Forall_hyps
   | |- Forall2 _ _ _ =>
diff --git a/theories/listset.v b/theories/listset.v
index 225034b9881570915e1d236cea3fee8d5bc79d7b..5c3df887ace11d4f7e482ae0a985fa5160f7dd3e 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -1,6 +1,6 @@
 (* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
-(** This file implements finite as unordered lists without duplicates
+(** This file implements finite set as unordered lists without duplicates
 removed. This implementation forms a monad. *)
 Require Export base decidable collections list.
 
@@ -48,8 +48,8 @@ Global Instance: FinCollection A (listset A).
 Proof.
   split.
   * apply _.
-  * symmetry. apply elem_of_remove_dups.
-  * intros. apply remove_dups_nodup.
+  * intros. apply elem_of_remove_dups.
+  * intros. apply NoDup_remove_dups.
 Qed.
 Global Instance: CollectionOps A (listset A).
 Proof.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index 2e9275eb64da97b625bcc239a9a9f998a004e116..b1af8fdcb54d10aa145326a60dab55351577b879 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -14,52 +14,34 @@ Arguments listset_nodup_prf {_} _.
 
 Section list_collection.
 Context {A : Type} `{∀ x y : A, Decision (x = y)}.
-
 Notation C := (listset_nodup A).
-Notation LS := ListsetNoDup.
 
 Instance listset_nodup_elem_of: ElemOf A C := λ x l, x ∈ listset_nodup_car l.
-Instance listset_nodup_empty: Empty C := LS [] (@NoDup_nil_2 _).
+Instance listset_nodup_empty: Empty C := ListsetNoDup [] (@NoDup_nil_2 _).
 Instance listset_nodup_singleton: Singleton A C := λ x,
-  LS [x] (NoDup_singleton x).
-Instance listset_nodup_difference: Difference C := λ l k,
-  let (l',Hl) := l in let (k',Hk) := k in LS _ (list_difference_nodup _ k' Hl).
-
-Definition listset_nodup_union_raw (l k : list A) : list A :=
-  list_difference l k ++ k.
-Lemma elem_of_listset_nodup_union_raw l k x :
-  x ∈ listset_nodup_union_raw l k ↔ x ∈ l ∨ x ∈ k.
-Proof.
-  unfold listset_nodup_union_raw.
-  rewrite elem_of_app, elem_of_list_difference.
-  intuition. case (decide (x ∈ k)); intuition.
-Qed.
-Lemma listset_nodup_union_raw_nodup l k :
-  NoDup l → NoDup k → NoDup (listset_nodup_union_raw l k).
-Proof.
-  intros. apply NoDup_app. repeat split.
-  * by apply list_difference_nodup.
-  * intro. rewrite elem_of_list_difference. intuition.
-  * done.
-Qed.
+  ListsetNoDup [x] (NoDup_singleton x).
 Instance listset_nodup_union: Union C := λ l k,
   let (l',Hl) := l in let (k',Hk) := k
-  in LS _ (listset_nodup_union_raw_nodup _ _ Hl Hk).
+  in ListsetNoDup _ (NoDup_list_union _ _ Hl Hk).
 Instance listset_nodup_intersection: Intersection C := λ l k,
   let (l',Hl) := l in let (k',Hk) := k
-  in LS _ (list_intersection_nodup _ k' Hl).
+  in ListsetNoDup _ (NoDup_list_intersection _ k' Hl).
+Instance listset_nodup_difference: Difference C := λ l k,
+  let (l',Hl) := l in let (k',Hk) := k
+  in ListsetNoDup _ (NoDup_list_difference _ k' Hl).
 Instance listset_nodup_intersection_with: IntersectionWith A C := λ f l k,
   let (l',Hl) := l in let (k',Hk) := k
-  in LS (remove_dups (list_intersection_with f l' k')) (remove_dups_nodup _).
+  in ListsetNoDup
+    (remove_dups (list_intersection_with f l' k')) (NoDup_remove_dups _).
 Instance listset_nodup_filter: Filter A C := λ P _ l,
-  let (l',Hl) := l in LS _ (filter_nodup P _ Hl).
+  let (l',Hl) := l in ListsetNoDup _ (NoDup_filter P _ Hl).
 
 Instance: Collection A C.
 Proof.
   split; [split | | ].
   * by apply not_elem_of_nil.
   * by apply elem_of_list_singleton.
-  * intros [??] [??] ?. apply elem_of_listset_nodup_union_raw.
+  * intros [??] [??] ?. apply elem_of_list_union.
   * intros [??] [??] ?. apply elem_of_list_intersection.
   * intros [??] [??] ?. apply elem_of_list_difference.
 Qed.
diff --git a/theories/mapset.v b/theories/mapset.v
index ae5741e56d292497a70ac7ec1179000ff3a01d88..6798d12d7c07ee59c2a25b7fd461ea8bb8a19d84 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -17,23 +17,23 @@ Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
 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,
-  match X1, X2 with Mapset m1, Mapset m2 => Mapset (m1 ∪ m2) end.
+  let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∪ m2).
 Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
-  match X1, X2 with Mapset m1, Mapset m2 => Mapset (m1 ∩ m2) end.
+  let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∩ m2).
 Instance mapset_difference: Difference (mapset M) := λ X1 X2,
-  match X1, X2 with Mapset m1, Mapset m2 => Mapset (m1 ∖ m2) end.
+  let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∖ m2).
 Instance mapset_elems: Elements K (mapset M) := λ X,
-  match X with Mapset m => fst <$> map_to_list m end.
+  let (m) := X in fst <$> map_to_list m.
 
 Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2.
 Proof.
-  split; [by intros; subst |].
+  split; [by intros ->|].
   destruct X1 as [m1], X2 as [m2]. simpl. intros E.
   f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E.
 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) : Decision (X1 = X2) | 1.
 Proof.
  refine
   match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end;
@@ -61,46 +61,42 @@ Proof.
     intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
     destruct (m2 !! x) as [[]|]; intuition congruence.
 Qed.
-
 Global Instance: PartialOrder (@subseteq (mapset M) _).
 Proof. split; try apply _. intros ????. apply mapset_eq. intuition. Qed.
-
 Global Instance: FinCollection K (mapset M).
 Proof.
   split.
   * apply _.
-  * unfold elements, elem_of at 1, mapset_elems, mapset_elem_of.
+  * unfold elements, elem_of at 2, mapset_elems, mapset_elem_of.
     intros [m] x. simpl. rewrite elem_of_list_fmap. split.
-    + intros. exists (x, ()). by rewrite elem_of_map_to_list.
     + intros ([y []] &?& Hy). subst. by rewrite <-elem_of_map_to_list.
+    + intros. exists (x, ()). by rewrite elem_of_map_to_list.
   * unfold elements, mapset_elems. intros [m]. simpl.
-    apply map_to_list_key_nodup.
+    apply NoDup_fst_map_to_list.
 Qed.
 
-Definition mapset_map_with `(f : bool → A → B) (X : mapset M) : M A → M B :=
-  match X with
-  | Mapset m => merge (λ x y,
+Definition mapset_map_with {A B} (f: bool → A → B) (X : mapset M) : 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
-  end.
-Definition mapset_dom_with `(f : A → bool) (m : M A) : mapset M :=
+    end) m.
+Definition mapset_dom_with {A} (f : A → bool) (m : M A) : mapset M :=
   Mapset $ merge (λ x _,
     match x with
     | Some a => if f a then Some () else None
     | None => None
     end) m (@empty (M A) _).
 
-Lemma lookup_mapset_map_with `(f : bool → A → B) X m i :
+Lemma lookup_mapset_map_with {A B} (f : bool → A → B) X m i :
   mapset_map_with f X m !! i = f (bool_decide (i ∈ X)) <$> m !! i.
 Proof.
   destruct X as [mX]. unfold mapset_map_with, elem_of, mapset_elem_of.
   rewrite lookup_merge by done. simpl.
   by case_bool_decide; destruct (mX !! i) as [[]|], (m !! i).
 Qed.
-Lemma elem_of_mapset_dom_with `(f : A → bool) m i :
+Lemma elem_of_mapset_dom_with {A} (f : A → bool) m i :
   i ∈ mapset_dom_with f m ↔ ∃ x, m !! i = Some x ∧ f x.
 Proof.
   unfold mapset_dom_with, elem_of, mapset_elem_of.
@@ -133,3 +129,4 @@ Hint Extern 1 (Difference (mapset _)) =>
   eapply @mapset_difference : typeclass_instances.
 Hint Extern 1 (Elements _ (mapset _)) =>
   eapply @mapset_elems : typeclass_instances.
+Arguments mapset_eq_dec _ _ _ _ : simpl never.
diff --git a/theories/natmap.v b/theories/natmap.v
index b0b44f74d25ba4c129676e2de0608f5cf8761367..1672c76934d13e7d80191792a51ad75d17378045 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -197,12 +197,12 @@ Proof.
     induction l1 as [|[x|] l1 IH]; intros [|[y|] l2] Hl1 Hl2 E; simpl in *.
     + done.
     + by specialize (E 0).
-    + destruct (natmap_wf_lookup (None :: l2)) as [i [??]]; auto with congruence.
+    + destruct (natmap_wf_lookup (None :: l2)) as (i&?&?); auto with congruence.
     + by specialize (E 0).
     + f_equal. apply (E 0). apply IH; eauto using natmap_wf_inv.
       intros i. apply (E (S i)).
     + by specialize (E 0).
-    + destruct (natmap_wf_lookup (None :: l1)) as [i [??]]; auto with congruence.
+    + destruct (natmap_wf_lookup (None :: l1)) as (i&?&?); auto with congruence.
     + by specialize (E 0).
     + f_equal. apply IH; eauto using natmap_wf_inv. intros i. apply (E (S i)).
   * done.
@@ -215,16 +215,67 @@ Proof.
   * intros ????? [??] [??] ?. by apply natmap_lookup_merge_raw.
 Qed.
 
-Lemma list_to_natmap_wf {A} (l : list A) : natmap_wf (Some <$> l).
-Proof. unfold natmap_wf. rewrite fmap_last. destruct (last l); simpl; eauto. Qed.
-Definition list_to_natmap {A} (l : list A) : natmap A :=
-  (Some <$> l) ↾ list_to_natmap_wf l.
+Fixpoint strip_Nones {A} (l : list (option A)) : list (option A) :=
+  match l with None :: l => strip_Nones l | _ => l end.
+
+Lemma list_to_natmap_wf {A} (l : list (option A)) :
+  natmap_wf (reverse (strip_Nones (reverse l))).
+Proof.
+  unfold natmap_wf. rewrite last_reverse.
+  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.
+Lemma list_to_natmap_spec {A} (l : list (option A)) i :
+  list_to_natmap l !! i = mjoin (l !! i).
+Proof.
+  unfold lookup at 1, natmap_lookup, list_to_natmap; simpl.
+  rewrite <-(reverse_involutive l) at 2. revert i.
+  induction (reverse l) as [|[x|] l' IH]; intros i; simpl; auto.
+  rewrite reverse_cons, IH. clear IH. revert i.
+  induction (reverse l'); intros [|?]; simpl; auto.
+Qed.
 
 (** Finally, we can construct sets of [nat]s satisfying extensional equality. *)
 Notation natset := (mapset natmap).
 Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
 Instance: FinMapDom nat natmap natset := mapset_dom_spec.
 
+(* Fixpoint avoids this definition from being unfolded *)
+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).
+
+Lemma of_bools_unfold βs :
+  of_bools βs
+  = Mapset $ list_to_natmap $ (λ β : bool, if β then Some () else None) <$> βs.
+Proof. by destruct βs. Qed.
+Lemma elem_of_of_bools βs i : i ∈ of_bools βs ↔ βs !! i = Some true.
+Proof.
+  rewrite of_bools_unfold; unfold elem_of, mapset_elem_of; simpl.
+  rewrite list_to_natmap_spec, list_lookup_fmap.
+  destruct (βs !! i) as [[]|]; compute; intuition congruence.
+Qed.
+Lemma elem_of_to_bools X i : to_bools X !! i = Some true ↔ i ∈ X.
+Proof.
+  unfold to_bools, elem_of, mapset_elem_of, lookup at 2, natmap_lookup; simpl.
+  destruct (mapset_car X) as [l ?]; simpl. rewrite list_lookup_fmap.
+  destruct (l !! i) as [[[]|]|]; compute; intuition congruence.
+Qed.
+Lemma of_to_bools X : of_bools (to_bools X) = X.
+Proof.
+  apply elem_of_equiv_L. intros i. by rewrite elem_of_of_bools,elem_of_to_bools.
+Qed.
+Lemma of_bools_union βs1 βs2 :
+  length βs1 = length βs2 →
+  of_bools (βs1 ||* βs2) = of_bools βs1 ∪ of_bools βs2.
+Proof.
+  rewrite <-Forall2_same_length; intros Hβs.
+  apply elem_of_equiv_L. intros i. rewrite elem_of_union, !elem_of_of_bools.
+  revert i. induction Hβs as [|[] []]; intros [|?]; naive_solver.
+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.
diff --git a/theories/nmap.v b/theories/nmap.v
index 2528e70f4664fd7b6f5da5ea2a36d367c29412f4..66cbb0a456e5349f99c187f453aaed779495e1de 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -58,8 +58,8 @@ Proof.
   * intros ? [[x|] t]; unfold map_to_list; simpl.
     + constructor.
       - rewrite elem_of_list_fmap. by intros [[??] [??]].
-      - apply (fmap_nodup _), map_to_list_nodup.
-    + apply (fmap_nodup _), map_to_list_nodup.
+      - by apply (NoDup_fmap _), NoDup_map_to_list.
+    + apply (NoDup_fmap _), NoDup_map_to_list.
   * intros ? t i x. unfold map_to_list. split.
     + destruct t as [[y|] t]; simpl.
       - rewrite elem_of_cons, elem_of_list_fmap.
diff --git a/theories/orders.v b/theories/orders.v
index f63f5b11cd6a223005b508d3868e5513fb547731..8f4599c4becdebdfaff8db2978f0e1bbe704fec0 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -488,12 +488,12 @@ Section bounded_join_sl.
 
   Section dec.
     Context `{∀ X Y : A, Decision (X ⊆ Y)}.
-    Lemma non_empty_union X Y : X ∪ Y ≢ ∅ → X ≢ ∅ ∨ Y ≢ ∅.
+    Lemma non_empty_union X Y : X ∪ Y ≢ ∅ ↔ X ≢ ∅ ∨ Y ≢ ∅.
     Proof. rewrite empty_union. destruct (decide (X ≡ ∅)); intuition. Qed.
     Lemma non_empty_union_list Xs : ⋃ Xs ≢ ∅ → Exists (≢ ∅) Xs.
     Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
     Context `{!LeibnizEquiv A}.
-    Lemma non_empty_union_L X Y : X ∪ Y ≠ ∅ → X ≠ ∅ ∨ Y ≠ ∅.
+    Lemma non_empty_union_L X Y : X ∪ Y ≠ ∅ ↔ X ≠ ∅ ∨ Y ≠ ∅.
     Proof. unfold_leibniz. apply non_empty_union. Qed.
     Lemma non_empty_union_list_L Xs : ⋃ Xs ≠ ∅ → Exists (≠ ∅) Xs.
     Proof. unfold_leibniz. apply non_empty_union_list. Qed.
diff --git a/theories/vector.v b/theories/vector.v
index 2583758bdbe5ea3a8f843781b5298b1e726bf01d..f7208fca9bea0b713395f5fa2d00cff1db5d85ce 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -88,7 +88,7 @@ Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
 Next Obligation.
   intros n. induction n; simpl; constructor.
   * rewrite elem_of_list_fmap. by intros (?&?&?).
-  * by apply (fmap_nodup _).
+  * by apply (NoDup_fmap _).
 Qed.
 Next Obligation.
   intros n i. induction i as [|n i IH]; simpl;
diff --git a/theories/zmap.v b/theories/zmap.v
index 52dc4fd0c1449d0750a4d62a30342466cdfdbbb2..605be57194f82a01643401087e2b709bcab1e50b 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -64,9 +64,9 @@ Proof.
     assert (NoDup ((prod_map Z.pos id <$> map_to_list t) ++
       prod_map Z.neg id <$> map_to_list t')).
     { apply NoDup_app; split_ands.
-      - apply (fmap_nodup _). apply map_to_list_nodup.
+      - apply (NoDup_fmap_2 _), NoDup_map_to_list.
       - intro. rewrite !elem_of_list_fmap. naive_solver.
-      - apply (fmap_nodup _). apply map_to_list_nodup. }
+      - apply (NoDup_fmap_2 _), NoDup_map_to_list. }
     destruct o; simpl; auto. constructor; auto.
     rewrite elem_of_app, !elem_of_list_fmap. naive_solver.
   * intros ? t i x. unfold map_to_list. split.